From 51a25fcbbcf1bac59af6dd8afb5312bf81ab2882 Mon Sep 17 00:00:00 2001 From: Vincent Beffara Date: Mon, 18 Mar 2024 15:17:30 +0100 Subject: [PATCH] Move contour integral stuff to another project --- HomotopyLifting.lean | 184 --------------------- RMT4.lean | 13 +- RMT4/Bunch.lean | 221 ------------------------- RMT4/Cellar.lean | 39 ----- RMT4/Covering.lean | 240 --------------------------- RMT4/Curvint.lean | 202 ----------------------- RMT4/Glue.lean | 120 -------------- RMT4/Lift.lean | 196 ---------------------- RMT4/LocallyConstant.lean | 65 -------- RMT4/Primitive.lean | 132 --------------- RMT4/RV.lean | 31 ---- RMT4/Subdivision.lean | 333 -------------------------------------- RMT4/cindex.lean | 2 - RMT4/etape2.lean | 2 - RMT4/pintegral.lean | 206 ----------------------- 15 files changed, 2 insertions(+), 1984 deletions(-) delete mode 100644 HomotopyLifting.lean delete mode 100644 RMT4/Bunch.lean delete mode 100644 RMT4/Cellar.lean delete mode 100644 RMT4/Covering.lean delete mode 100644 RMT4/Curvint.lean delete mode 100644 RMT4/Glue.lean delete mode 100644 RMT4/Lift.lean delete mode 100644 RMT4/LocallyConstant.lean delete mode 100644 RMT4/Primitive.lean delete mode 100644 RMT4/RV.lean delete mode 100644 RMT4/Subdivision.lean delete mode 100644 RMT4/pintegral.lean diff --git a/HomotopyLifting.lean b/HomotopyLifting.lean deleted file mode 100644 index 60da722..0000000 --- a/HomotopyLifting.lean +++ /dev/null @@ -1,184 +0,0 @@ -/- -Copyright (c) 2023 Junyan Xu. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Junyan Xu --/ -import Mathlib.Topology.Covering -import Mathlib.Topology.UnitInterval -/-! - -# The Homotopy lifting property of covering maps - -Currently, this file only proves uniqueness of lifting, not existence, -but under some more general conditions than covering maps, in order to -apply to situations such as the monodromy theorem for analytic continuations. --/ - -open Topology unitInterval - -variable {E X A : Type*} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] - {p : C(E,X)} - -/-- If every `e : E` has an open neighborhood on which `p : E → X` is injective such that - `p⁻¹(p(U))\U` is also open, and if `A` is a connected space, - then two lifts `g₁,g₂ : A → E` of a map `f : A → X` are equal if they agree at one point. -/ -theorem ContinuousMap.eq_of_comp_eq [PreconnectedSpace A] - (hp : ∀ e : E, ∃ U, e ∈ U ∧ IsOpen U ∧ U.InjOn p ∧ IsOpen (p ⁻¹' (p '' U) \ U)) - (g₁ g₂ : C(A,E)) (he : p.comp g₁ = p.comp g₂) - (a : A) (ha : g₁ a = g₂ a) : g₁ = g₂ := by - have := IsClopen.eq_univ (s := {a | g₁ a = g₂ a}) ⟨?_, ?_⟩ ⟨a, ha⟩ - · ext a; apply this.symm ▸ Set.mem_univ a - /- Since A is connected and s := {a | g₁ a = g₂ a} inhabited by a, - we just need to show that s is open and closed. -/ - · refine isOpen_iff_mem_nhds.mpr (fun a ha ↦ mem_nhds_iff.mpr ?_) - /- Given a point a where g₁ and g₂ agree, - take an open neighborhood U of g₁(a) = g₂(a) on which p is injective. - Then g₁ and g₂ agree on the open neighborhood g₁⁻¹(U) ∩ g₂⁻¹(U) of a. -/ - obtain ⟨U, haU, hoU, hi, -⟩ := hp (g₁ a) - exact ⟨g₁ ⁻¹' U ∩ g₂ ⁻¹' U, fun a' ha ↦ hi ha.1 ha.2 (FunLike.congr_fun he a'), - (g₁.2.isOpen_preimage _ hoU).inter (g₂.2.isOpen_preimage _ hoU), haU, ha.subst haU⟩ - · simp_rw [← isOpen_compl_iff, isOpen_iff_mem_nhds, mem_nhds_iff] - intro a ha - /- Given a point a where g₁ and g₂ doesn't agree, - take an open neighborhood U of g₁(a) on which p is injective such that p⁻¹(p(U))\U is open. - Then g₁ and g₂ doesn't agree on any point - in the neighborhood g₁⁻¹(U) ∩ g₂⁻¹(p⁻¹(p(U))\U) of a. -/ - obtain ⟨U, hU₁, hoU, hi, compl_open⟩ := hp (g₁ a) - have := FunLike.congr_fun he a - refine ⟨_, fun a' ha' he ↦ ha'.2.2 (he ▸ ha'.1), (g₁.continuous.isOpen_preimage _ hoU).inter - (g₂.continuous.isOpen_preimage _ compl_open), hU₁, ?_, fun hU₂ ↦ ha (hi hU₁ hU₂ this)⟩ - apply this ▸ Set.mem_image_of_mem p hU₁ - -theorem lebesgue_number_lemma_unitInterval {ι} {c : ι → Set I} (hc₁ : ∀ i, IsOpen (c i)) - (hc₂ : Set.univ ⊆ ⋃ i, c i) : ∃ t : ℕ → I, t 0 = 0 ∧ Monotone t ∧ - (∀ n, ∃ i, Set.Icc (t n) (t <| n + 1) ⊆ c i) ∧ ∃ n, ∀ m ≥ n, t m = 1 := by - obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂ - refine ⟨fun n ↦ Set.projIcc 0 1 zero_le_one (n * (δ/2)), ?_, fun n m hnm ↦ ?_, fun n ↦ ?_, ?_⟩ - · dsimp only; rw [Nat.cast_zero, zero_mul, Set.projIcc_left]; rfl - · apply Set.monotone_projIcc - rw [mul_le_mul_right (div_pos δ_pos zero_lt_two)] - exact_mod_cast hnm - · obtain ⟨i, hsub⟩ := ball_subset (Set.projIcc 0 1 zero_le_one (n * (δ/2))) trivial - refine ⟨i, fun x hx ↦ hsub ?_⟩ - rw [Metric.mem_ball] - apply (abs_eq_self.mpr _).trans_lt - · apply (sub_le_sub_right _ _).trans_lt - on_goal 3 => exact hx.2 - refine (max_sub_max_le_max _ _ _ _).trans_lt (max_lt (by rwa [sub_zero]) ?_) - refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans_lt (max_lt ?_ ?_) - · rwa [sub_self, abs_zero] - · rw [← sub_mul, Nat.cast_succ, add_sub_cancel', one_mul, abs_lt] - constructor <;> linarith only [δ_pos] - · exact sub_nonneg_of_le hx.1 - · refine ⟨Nat.ceil (δ/2)⁻¹, fun n hn ↦ (Set.projIcc_eq_right zero_lt_one).mpr ?_⟩ - rwa [GE.ge, Nat.ceil_le, inv_pos_le_iff_one_le_mul (div_pos δ_pos zero_lt_two)] at hn - -instance : BoundedOrder I := Set.Icc.boundedOrder zero_le_one - - ---instance {α} [TopologicalSpace α] [Preorder α] [CompactIccSpace α] {a b : α} : --- CompactIccSpace (Set.Icc a b) := by - -- closed subset of compact space - -- Ioo, Ioc, Ico, Iio, etc... - - -/-- If `p : E → X` is a local homeomorphism, and if `g : I × A → E` is a lift of `f : C(I × A, X)` - continuous on `{0} × A ∪ I × {a}` for some `a : A`, then there exists a neighborhood `N ∈ 𝓝 a` - and `g' : I × A → E` continuous on `I × N` that agrees with `g` on `{0} × A ∪ I × {a}`. - The proof follows Hatcher, Proof of Theorem 1.7, p.30. - - This lemma should also be true for an arbitrary space in place of `I` if `A` is locally connected, - and if `hp` furthermore satisfies the property in `ContinuousMap.eq_of_comp_eq` which guarantees - uniqueness and therefore well-definedness on the intersections. -/ -lemma IsLocallyHomeomorph.exists_lift_nhds {p : E → X} (hp : IsLocallyHomeomorph p) - {f : C(I × A, X)} {g : I × A → E} (g_lifts : p ∘ g = f) - (cont_0 : Continuous (g ⟨0, ·⟩)) (a : A) (cont_a : Continuous (g ⟨·, a⟩)) : - ∃ N ∈ 𝓝 a, ∃ g' : I × A → E, ContinuousOn g' (Set.univ ×ˢ N) ∧ p ∘ g' = f ∧ - (∀ a, g' (0, a) = g (0, a)) ∧ ∀ t, g' (t, a) = g (t, a) := by - /- For every `e : E`, we can upgrade `p` to a LocalHomeomorph `q e` around `e`. -/ - choose q mem_source hpq using hp - obtain ⟨t, t_0, t_mono, t_sub, n_max, h_max⟩ := lebesgue_number_lemma_unitInterval - (fun e ↦ cont_a.isOpen_preimage _ (q e).open_source) - (fun t _ ↦ Set.mem_iUnion.mpr ⟨g (t, a), mem_source _⟩) - suffices : ∀ n, ∃ N, a ∈ N ∧ IsOpen N ∧ ∃ g' : I × A → E, ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧ - p ∘ g' = f ∧ (∀ a, g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a) - · obtain ⟨N, haN, N_open, hN⟩ := this n_max - simp_rw [h_max _ le_rfl] at hN - refine ⟨N, N_open.mem_nhds haN, ?_⟩; convert hN - · rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩ - · rw [imp_iff_right]; exact le_top - refine Nat.rec ⟨_, Set.mem_univ a, isOpen_univ, g, ?_, g_lifts, fun a ↦ rfl, fun _ _ ↦ rfl⟩ - (fun n ⟨N, haN, N_open, g', cont_g', g'_lifts, g'_0, g'_a⟩ ↦ ?_) - · refine (cont_0.comp continuous_snd).continuousOn.congr (fun ta ⟨ht, _⟩ ↦ ?_) - rw [t_0, Set.Icc_self, Set.mem_singleton_iff] at ht; rw [← ta.eta, ht]; rfl - obtain ⟨e, h_sub⟩ := t_sub n - have : Set.Icc (t n) (t (n+1)) ×ˢ {a} ⊆ f ⁻¹' (q e).target - · rintro ⟨t0, a'⟩ ⟨ht, ha⟩ - rw [Set.mem_singleton_iff] at ha; dsimp only at ha - rw [← g_lifts, hpq e, ha] - exact (q e).map_source (h_sub ht) - obtain ⟨u, v, -, v_open, hu, hav, huv⟩ := generalized_tube_lemma isClosed_Icc.isCompact - isCompact_singleton (f.continuous.isOpen_preimage _ (q e).open_target) this - classical - refine ⟨_, ?_, v_open.inter <| (cont_g'.comp (Continuous.Prod.mk <| t n).continuousOn - fun a ha ↦ ⟨?_, ha⟩).preimage_open_of_open N_open (q e).open_source, - fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then (q e).symm (f ta) else g ta, - ContinuousOn.if (fun ta ⟨⟨_, hav, _, ha⟩, hfr⟩ ↦ ?_) (cont_g'.mono fun ta ⟨hta, ht⟩ ↦ ?_) ?_, - ?_, fun a ↦ ?_, fun t0 htn1 ↦ ?_⟩ - · refine ⟨Set.singleton_subset_iff.mp hav, haN, ?_⟩ - change g' (t n, a) ∈ (q e).source; rw [g'_a _ le_rfl] - exact h_sub ⟨le_rfl, t_mono n.le_succ⟩ - · rw [← t_0]; exact ⟨t_mono n.zero_le, le_rfl⟩ - · have ht := Set.mem_setOf.mp (frontier_le_subset_eq continuous_fst continuous_const hfr) - have : f ta ∈ (q e).target := huv ⟨hu (by rw [ht]; exact ⟨le_rfl, t_mono n.le_succ⟩), hav⟩ - rw [if_pos this] - apply (q e).injOn (by rw [← ta.eta, ht]; exact ha) ((q e).map_target this) - rw [(q e).right_inv this, ← hpq e]; exact congr_fun g'_lifts ta - · rw [(isClosed_le continuous_fst continuous_const).closure_eq] at ht - exact ⟨⟨hta.1.1, ht⟩, hta.2.2.1⟩ - · simp_rw [not_le]; exact (ContinuousOn.congr ((q e).continuous_invFun.comp f.2.continuousOn - fun _ h ↦ huv ⟨hu ⟨h.2, h.1.1.2⟩, h.1.2.1⟩) - fun _ h ↦ if_pos <| huv ⟨hu ⟨h.2, h.1.1.2⟩, h.1.2.1⟩).mono - (Set.inter_subset_inter_right _ <| closure_lt_subset_le continuous_const continuous_fst) - · ext ta; rw [Function.comp_apply]; split_ifs with _ hv - · exact congr_fun g'_lifts ta - · rw [hpq e, (q e).right_inv hv] - · exact congr_fun g_lifts ta - · rw [← g'_0]; exact if_pos bot_le - · dsimp only; split_ifs with htn hf - · exact g'_a t0 htn - · apply (q e).injOn ((q e).map_target hf) (h_sub ⟨le_of_not_ge htn, htn1⟩) - rw [(q e).right_inv hf, ← hpq e]; exact (congr_fun g_lifts _).symm - · rfl - -lemma IsLocallyHomeomorph.continuous_lift {p : E → X} (loc_homeo : IsLocallyHomeomorph p) - (hp : ∀ e : E, ∃ U, e ∈ U ∧ IsOpen U ∧ U.InjOn p ∧ IsOpen (p ⁻¹' (p '' U) \ U)) - {f : C(I × A, X)} {g : I × A → E} (g_lifts : p ∘ g = f) - (cont_0 : Continuous (g ⟨0, ·⟩)) (cont_A : ∀ a, Continuous (g ⟨·, a⟩)) : Continuous g := by - rw [continuous_iff_continuousAt] - intro ⟨t, a⟩ - obtain ⟨N, haN, g', cont_g', g'_lifts, g'_0, -⟩ := - loc_homeo.exists_lift_nhds g_lifts cont_0 a (cont_A a) - refine (cont_g'.congr fun ⟨t, a⟩ ⟨_, ha⟩ ↦ ?_).continuousAt (prod_mem_nhds Filter.univ_mem haN) - refine FunLike.congr_fun (ContinuousMap.eq_of_comp_eq (p := ⟨_, loc_homeo.continuous⟩) hp - ⟨_, cont_A a⟩ ⟨_, cont_g'.comp_continuous (Continuous.Prod.mk_left a) (fun _ ↦ ⟨trivial, ha⟩)⟩ - ?_ 0 (g'_0 a).symm) t - ext t; apply congr_fun (g_lifts.trans g'_lifts.symm) - -lemma IsCoveringMap.exists_nhds_clopen {p : E → X} (hp : IsCoveringMap p) (e : E) : - ∃ U, e ∈ U ∧ IsOpen U ∧ U.InjOn p ∧ IsOpen (p ⁻¹' (p '' U) \ U) := by - obtain ⟨hd, t, ht⟩ := hp (p e) - refine ⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e).2}, ⟨by rwa [t.source_eq], rfl⟩, t.continuous_toFun - |>.preimage_open_of_open t.open_source (continuous_snd.isOpen_preimage _ <| isOpen_discrete _), - fun e₁ h₁ e₂ h₂ he ↦ t.injOn h₁.1 h₂.1 (Prod.ext ?_ <| h₁.2.trans h₂.2.symm), ?_⟩ - · rwa [t.proj_toFun e₁ h₁.1, t.proj_toFun e₂ h₂.1] - convert t.continuous_toFun.preimage_open_of_open t.open_source - (continuous_snd.isOpen_preimage _ <| isOpen_discrete {(t e).2}ᶜ) using 1 - ext e₀ - rw [t.source_eq, Set.image_preimage_inter, Set.preimage_inter, ← Set.inter_diff_distrib_left] - refine ⟨fun h ↦ ⟨h.1, h.2.2⟩, fun h ↦ ⟨h.1, ?_, h.2⟩⟩ - let x := (p e₀, (t e).2); have : x ∈ t.target - · rw [t.target_eq]; exact ⟨h.1, trivial⟩ - refine ⟨t.invFun (p e₀, (t e).2), (congr_arg Prod.snd <| t.right_inv this).trans rfl, ?_⟩ - rw [← t.proj_toFun] - exacts [congr_arg Prod.fst (t.right_inv this), t.map_target this] diff --git a/RMT4.lean b/RMT4.lean index 376ad8b..fbf7ded 100644 --- a/RMT4.lean +++ b/RMT4.lean @@ -1,21 +1,12 @@ import Mathlib.Analysis.Complex.OpenMapping import RMT4.Basic -import RMT4.Bunch import RMT4.cindex -import RMT4.Covering -import RMT4.Curvint import RMT4.defs import RMT4.deriv_inj import RMT4.etape2 -import RMT4.Glue import RMT4.has_sqrt import RMT4.hurwitz -import RMT4.Lift -import RMT4.LocallyConstant import RMT4.montel -import RMT4.pintegral -import RMT4.Primitive -import RMT4.Subdivision import RMT4.to_mathlib import RMT4.uniform @@ -35,8 +26,8 @@ lemma isCompact_𝓜 (hU : IsOpen U) : IsCompact (𝓜 U) := by simpa only [𝓑_const] using isCompact_𝓑 hU (fun _ _ => isCompact_closedBall 0 1) lemma IsClosed_𝓜 (hU : IsOpen U) : IsClosed (𝓜 U) := by - suffices h : IsClosed {f : 𝓒 U | MapsTo f U (closedBall 0 1)} - · exact (isClosed_𝓗 hU).inter h + suffices h : IsClosed {f : 𝓒 U | MapsTo f U (closedBall 0 1)} by + exact (isClosed_𝓗 hU).inter h simp_rw [MapsTo, setOf_forall] refine isClosed_biInter (λ z hz => isClosed_ball.preimage ?_) exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U) diff --git a/RMT4/Bunch.lean b/RMT4/Bunch.lean deleted file mode 100644 index 09b4c33..0000000 --- a/RMT4/Bunch.lean +++ /dev/null @@ -1,221 +0,0 @@ -import Mathlib.Topology.Basic -import Mathlib.Data.Set.Image -import Mathlib.Topology.MetricSpace.Basic - -open Topology Filter Metric TopologicalSpace Set Subtype - -structure Bunch (ι α β : Type) [TopologicalSpace α] where - S : ι → Set α - F : ι → α → β - cmp i j : IsOpen { a ∈ S i ∩ S j | F i a = F j a } - -namespace Bunch - -variable {ι α β : Type} [TopologicalSpace α] {i₁ i₂ i j : ι} {a : α} {b : β} {s t : Set α} - -instance : CoeFun (Bunch ι α β) (λ _ => ι → α → β) := ⟨Bunch.F⟩ - -def space (_ : Bunch ι α β) := α × β - -def idx (B : Bunch ι α β) (z : B.space) : Set ι := { i | z.1 ∈ B.S i ∧ B i z.1 = z.2 } - -def tile (B : Bunch ι α β) (i : ι) (s : Set α) : Set B.space := (λ x => (x, B i x)) '' s - -def range (B : Bunch ι α β) : Set (B.space) := { z | Nonempty (B.idx z) } - -def reaches (B : Bunch ι α β) (is : ι × Set α) (z : B.space) := is.1 ∈ B.idx z ∧ is.2 ∈ 𝓝 z.1 - -lemma opn (B : Bunch ι α β) (i : ι) : IsOpen (B.S i) := by simpa using B.cmp i i - -variable {B : Bunch ι α β} {s s₁ s₂ : Set B.space} {z : B.space} - -lemma S_mem_nhd (hi : i ∈ B.idx z) : B.S i ∈ 𝓝 z.1 := B.opn i |>.mem_nhds hi.1 - -lemma eq_of_mem_tile (h : z ∈ B.tile i t) : B i z.1 = z.2 := by - obtain ⟨x, _, rfl⟩ := h ; rfl - -lemma tile_mono {s t : Set α} (h : s ⊆ t) : B.tile i s ⊆ B.tile i t := image_subset _ h - -lemma tile_congr {s : Set α} (h : EqOn (B i) (B j) s) : B.tile i s = B.tile j s := - image_congr (λ x hx => by rw [h hx]) - -lemma subset_iff_forall (a : Set α) (b : Set β) (f : α → β) : f '' a ⊆ b ↔ ∀ x ∈ a, f x ∈ b := by - rw [image_subset_iff] ; rfl - -lemma eventuallyEq (hi : a ∈ B.S i) (hj : a ∈ B.S j) (h : B i a = B j a) : - ∀ᶠ b in 𝓝 a, B i b = B j b := - (eventually_and.1 <| (B.cmp i j).mem_nhds ⟨⟨hi, hj⟩, h⟩).2 - -lemma tile_inter {s₁ s₂ : Set α} (hi₁ : i₁ ∈ B.idx z) (hi₂ : i₂ ∈ B.idx z) (hi : i ∈ B.idx z) - (h₁ : s₁ ∈ 𝓝 z.1) (h₂ : s₂ ∈ 𝓝 z.1) : - ∃ s ∈ 𝓝 z.1, B.tile i s ⊆ B.tile i₁ s₁ ∩ B.tile i₂ s₂ := by - suffices h : ∀ᶠ b in 𝓝 z.1, (b, B i b) ∈ B.tile i₁ s₁ ∩ B.tile i₂ s₂ - by simpa only [eventually_iff_exists_mem, ← subset_iff_forall] using h - have l1 := eventuallyEq hi₁.1 hi.1 (hi₁.2.trans hi.2.symm) - have l2 := eventuallyEq hi₂.1 hi.1 (hi₂.2.trans hi.2.symm) - filter_upwards [h₁, h₂, l1, l2] with b e1 e2 e3 e4 - exact ⟨⟨b, e1, by simp only [e3]⟩, ⟨b, e2, by simp only [e4]⟩⟩ - -lemma isBasis (hz : z ∈ B.range) : - IsBasis (λ is => B.reaches is z) (λ is => B.tile is.1 is.2) where - nonempty := by - obtain ⟨i, hi⟩ := hz - refine ⟨⟨i, univ⟩, hi, univ_mem⟩ - inter := by - rintro i j ⟨hi1, hi2⟩ ⟨hj1, hj2⟩ - obtain ⟨s, hs1, hs2⟩ := tile_inter hi1 hj1 hi1 hi2 hj2 - refine ⟨⟨i.1, s⟩, ⟨⟨hi1, hs1⟩, hs2⟩⟩ - -def nhd (z : B.space) : Filter B.space := open Classical in - if h : Nonempty (B.idx z) then (isBasis h).filter else pure z - -instance : TopologicalSpace B.space := TopologicalSpace.mkOfNhds nhd - -lemma mem_nhd (h : Nonempty (B.idx z)) : - s ∈ nhd z ↔ ∃ i ∈ B.idx z, ∃ v ∈ 𝓝 z.1, B.tile i v ⊆ s := by - simp only [nhd, h, dite_true] - simp [(isBasis h).mem_filter_iff, reaches, and_assoc] - -theorem eventually_apply_mem {f : α → β} {t : Set β} : - (∀ᶠ x in 𝓝 a, f x ∈ t) ↔ (∃ s ∈ 𝓝 a, s ⊆ f ⁻¹' t) := - eventually_iff_exists_mem - -theorem eventually_mem_iff_tile : - (∀ᶠ b in 𝓝 a, (b, B j b) ∈ s) ↔ (∃ v ∈ 𝓝 a, tile B j v ⊆ s) := by - simp [tile, ← eventually_apply_mem] - -lemma tile_mem_nhd' {s : Set α} (hi : i ∈ B.idx z) (hs : s ∈ 𝓝 z.1) : B.tile i s ∈ nhd z := by - have : Nonempty (B.idx z) := ⟨_, hi⟩ - simp only [nhd, this, dite_true] - simpa only [IsBasis.mem_filter_iff] using ⟨(i, s), ⟨hi, hs⟩, subset_rfl⟩ - -lemma mem_nhd_open (hz : Nonempty (B.idx z)) (h : s ∈ nhd z) : - ∃ i ∈ B.idx z, ∃ v ∈ 𝓝 z.1, IsOpen v ∧ B.tile i v ⊆ s := by - obtain ⟨i, hi1, t, hi3, hi4⟩ := (mem_nhd hz).1 h - obtain ⟨s', ⟨h1, h2⟩, h3⟩ := nhds_basis_opens' z.1 |>.mem_iff.1 hi3 - exact ⟨i, hi1, s', h1, h2, tile_mono h3 |>.trans hi4⟩ - -theorem pure_le (z : B.space) : pure z ≤ nhd z := by - by_cases h : Nonempty (B.idx z) - · intro s hs - obtain ⟨i, hi1, hi2, hi3, hi4⟩ := (mem_nhd h).1 hs - exact hi4 ⟨z.1, mem_of_mem_nhds hi3, by simp [hi1.2]⟩ - · simp only [nhd, h, dite_false] ; rfl - -theorem nhd_is_nhd (a : space B) (s : Set (space B)) (hs : s ∈ nhd a) : - ∃ t ∈ nhd a, t ⊆ s ∧ ∀ b ∈ t, s ∈ nhd b := by - by_cases h : Nonempty (B.idx a) - · obtain ⟨i, hi1, s₀, hi2, hi3, hi4⟩ := mem_nhd_open h hs - refine ⟨B.tile i (s₀ ∩ B.S i), ?_, ?_, ?_⟩ - · exact tile_mem_nhd' hi1 <| inter_mem hi2 <| S_mem_nhd hi1 - · exact tile_mono (inter_subset_left _ _) |>.trans hi4 - · rintro b ⟨c, hb1, rfl⟩ - refine mem_of_superset ?_ hi4 - refine tile_mem_nhd' ⟨?_, rfl⟩ ?_ - · exact inter_subset_right _ _ hb1 - · exact hi3.mem_nhds <| inter_subset_left _ _ hb1 - · have hs' := hs - simp only [nhd, h, dite_false, mem_pure] at hs' - refine ⟨{a}, ?_, by simp [hs'], ?_⟩ - · simp only [nhd, h, dite_false] ; simp - · simp [hs] - -lemma nhds_eq_nhd : 𝓝 z = nhd z := by - refine nhds_mkOfNhds _ _ pure_le ?_ - intro a s hs - obtain ⟨t, h1, _, h3⟩ := nhd_is_nhd a s hs -- TODO simplify `nhd_is_nhd` - apply eventually_of_mem h1 h3 - -lemma mem_nhds_tfae (h : Nonempty (B.idx z)) : List.TFAE [ - s ∈ 𝓝 z, - s ∈ nhd z, - ∃ i ∈ B.idx z, ∀ᶠ a in 𝓝 z.1, (a, B i a) ∈ s, - ∃ i ∈ B.idx z, ∃ t ∈ 𝓝 z.1, B.tile i t ⊆ s - ] := by - tfae_have 1 ↔ 2 ; simp [nhds_eq_nhd] - tfae_have 2 ↔ 4 ; exact mem_nhd h - tfae_have 3 ↔ 4 ; simp [eventually_mem_iff_tile] - tfae_finish - -@[simp] lemma nhds_eq_pure (h : ¬ Nonempty (B.idx z)) : 𝓝 z = pure z := by - simp only [nhds_eq_nhd, nhd, h, dite_false] - -lemma tile_mem_nhd {s : Set α} (hi : i ∈ B.idx z) (hs : s ∈ 𝓝 z.1) : B.tile i s ∈ 𝓝 z := by - simpa [nhds_eq_nhd] using tile_mem_nhd' hi hs - -def p (B : Bunch ι α β) (z : B.space) : α := z.1 - -lemma discreteTopology : DiscreteTopology (B.p ⁻¹' {a}) := by - simp [discreteTopology_iff_singleton_mem_nhds, nhds_induced] - rintro ⟨z₁, z₂⟩ rfl - by_cases h : Nonempty (B.idx (z₁, z₂)) - · obtain ⟨i, h1, rfl : B i z₁ = z₂⟩ := h - refine ⟨B.tile i <| B.S i, ?_, ?_⟩ - · exact tile_mem_nhd ⟨h1, rfl⟩ <| S_mem_nhd ⟨h1, rfl⟩ - · rintro x rfl ⟨u, _, rfl⟩ ; rfl - · refine ⟨{(z₁, z₂)}, ?_, by simp⟩ - simp only [nhds_eq_nhd, nhd, h, dite_false, mem_pure, mem_singleton] - -lemma continuous_p : Continuous B.p := by - rw [continuous_iff_continuousAt] ; intro x s hs - by_cases h : Nonempty (B.idx x) - · obtain ⟨i, hi⟩ := h - apply mem_of_superset <| tile_mem_nhd hi hs - rintro y ⟨x, hx, rfl⟩ ; exact hx - · simpa only [nhds_eq_nhd, nhd, h, dite_false, Filter.map_pure, mem_pure] using mem_of_mem_nhds hs - -end Bunch - -section lift - -variable {ι α β γ : Type} [TopologicalSpace α] {B : Bunch ι α β} - {γ : Type} [TopologicalSpace γ] [PreconnectedSpace γ] - -def IsLiftOf (g : γ → B.space) (f : γ → α) : Prop := Continuous g ∧ ∀ x, B.p (g x) = f x - -lemma eventually_mem_tile {γ : Type} [TopologicalSpace γ] {f : γ → B.space} {x : γ} - (hf : ContinuousAt f x) {i : ι} (hi : i ∈ B.idx (f x)) : - ∀ᶠ y in 𝓝 x, (f y).2 = B.F i (f y).1 := by - refine eventually_of_mem (hf.preimage_mem_nhds <| B.tile_mem_nhd hi <| B.S_mem_nhd hi) ?_ - exact λ x hx => by simp [B.eq_of_mem_tile hx] - -theorem eventually_eq_of_lift {γ : Type} [TopologicalSpace γ] {f : γ → α} - {g₁ g₂ : γ → Bunch.space B} (h₁ : IsLiftOf g₁ f) (h₂ : IsLiftOf g₂ f) {x : γ} - (hx : g₁ x = g₂ x) (h1 : Nonempty ↑(Bunch.idx B (g₁ x))) : g₁ =ᶠ[𝓝 x] g₂ := by - obtain ⟨i1, hi1⟩ := h1 - filter_upwards [eventually_mem_tile (h₁.1.continuousAt) hi1, - eventually_mem_tile (h₂.1.continuousAt) (hx ▸ hi1)] with y r1 r2 - have r4 : (g₁ y).1 = f y := h₁.2 y - have r5 : (g₂ y).1 = f y := h₂.2 y - rw [Prod.ext_iff] - simp [r1, r2, r4, r5] - -theorem eventually_eq_of_lift' {γ : Type} [TopologicalSpace γ] {f : γ → α} {x : γ} - {g₁ g₂ : γ → Bunch.space B} (h₁ : IsLiftOf g₁ f) (h₂ : IsLiftOf g₂ f) (hx : g₁ x = g₂ x) : - g₁ =ᶠ[𝓝 x] g₂ := by - by_cases h1 : Nonempty ↑(Bunch.idx B (g₁ x)) - · obtain ⟨i1, hi1⟩ := h1 - filter_upwards [eventually_mem_tile (h₁.1.continuousAt) hi1, - eventually_mem_tile (h₂.1.continuousAt) (hx ▸ hi1)] with y r1 r2 - have r4 : (g₁ y).1 = f y := h₁.2 y - have r5 : (g₂ y).1 = f y := h₂.2 y - rw [Prod.ext_iff] - simp [r1, r2, r4, r5] - · have h2 := h₁.1.tendsto x - have h3 := h₂.1.tendsto x - simp [Bunch.nhds_eq_pure h1, Bunch.nhds_eq_pure (hx ▸ h1), tendsto_pure] at h2 h3 - filter_upwards [h2, h3] with y h4 h5 - simp [hx, h4, h5] - -theorem isOpen_eq_of_lift {γ : Type} [TopologicalSpace γ] {f : γ → α} {g₁ g₂ : γ → Bunch.space B} - (h₁ : IsLiftOf g₁ f) (h₂ : IsLiftOf g₂ f) : IsOpen {x | g₁ x = g₂ x} := by - simpa only [isOpen_iff_eventually] using λ _ => eventually_eq_of_lift' h₁ h₂ - -lemma lift_congr (f : γ → α) (g₁ g₂ : γ → B.space) (h₁ : IsLiftOf g₁ f) (h₂ : IsLiftOf g₂ f) - {x₀ : γ} (h₀ : g₁ x₀ = g₂ x₀) : g₁ = g₂ := by - let s : Set γ := { x | g₁ x = g₂ x } - have h2 : IsClosed s := by sorry - have h3 : IsClopen s := ⟨h2, isOpen_eq_of_lift h₁ h₂⟩ - have h4 : s = univ := (isClopen_iff.1 h3).resolve_left <| Nonempty.ne_empty ⟨x₀, h₀⟩ - exact funext (λ x => (h4 ▸ mem_univ x : x ∈ s)) -end lift diff --git a/RMT4/Cellar.lean b/RMT4/Cellar.lean deleted file mode 100644 index 9f2ba26..0000000 --- a/RMT4/Cellar.lean +++ /dev/null @@ -1,39 +0,0 @@ -import RMT4.Lift - -open Set Topology Metric unitInterval Filter ContinuousMap - -variable {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] - {f : E → X} {γ : C(I, X)} {x : X} {A : E} {t t₁ t₂ : I} {Γ Γ₁ Γ₂ : C(I, E)} - -lemma prekey {T : Trivialization (f ⁻¹' {x}) f} [DiscreteTopology (f ⁻¹' {x})] {z : E} - (h : z ∈ T.source) : ∀ᶠ w in 𝓝 z, T w = (f w, (T z).2) := by - have l1 : {(T z).2} ∈ 𝓝 (T z).2 := by simp only [nhds_discrete, mem_pure, mem_singleton_iff] - have l2 : ∀ᶠ w in 𝓝 z, (T w).2 = (T z).2 := continuousAt_snd.comp (T.continuousAt h) l1 - filter_upwards [T.open_source.mem_nhds h, l2] with s hs r2 using Prod.ext (T.coe_fst hs) r2 - -lemma key {T : Trivialization (f ⁻¹' {x}) f} [DiscreteTopology (f ⁻¹' {x})] (h : Γ t ∈ T.source) : - ∀ᶠ s in 𝓝 t, T (Γ s) = (f (Γ s), (T (Γ t)).2) := Γ.continuousAt _ (prekey h) - -lemma key2 {T : Trivialization (f ⁻¹' {x}) f} [DiscreteTopology (f ⁻¹' {x})] (h : Γ t ∈ T.source) : - ∀ᶠ s in 𝓝 t, Γ s = T.invFun (f (Γ s), (T (Γ t)).2) := by - filter_upwards [key h, Γ.continuousAt _ <| T.open_source.mem_nhds h] with s r1 r2 - simpa only [← r1] using (T.left_inv r2).symm - -lemma locally_eq (hf : IsCoveringMap f) (h1 : Γ₁ t = Γ₂ t) (h2 : f ∘ Γ₁ =ᶠ[𝓝 t] f ∘ Γ₂) : - Γ₁ =ᶠ[𝓝 t] Γ₂ := by - obtain ⟨l1, T, l2⟩ := hf (f (Γ₁ t)) - rw [← T.mem_source] at l2 - filter_upwards [key2 l2, key2 (Γ := Γ₂) (T := T) (h1 ▸ l2), h2] with s r2 r3 (r4 : f _ = f _) - rw [r2, r3] ; congr - -lemma locally_eq_iff (hf : IsCoveringMap f) (h2 : f ∘ Γ₁ =ᶠ[𝓝 t] f ∘ Γ₂) : - ∀ᶠ s in 𝓝 t, Γ₁ s = Γ₂ s ↔ Γ₁ t = Γ₂ t := by - obtain ⟨l1, T, l2⟩ := hf (f (Γ₁ t)) - have : f _ = f _ := h2.self_of_nhds - have l3 : f (Γ₂ t) ∈ T.baseSet := by simp [← show f (Γ₁ t) = f (Γ₂ t) from this, l2] - rw [← T.mem_source] at l2 l3 - filter_upwards [key2 l2, key2 l3, key l2, key l3, h2] with s r2 r3 r4 r5 (r6 : f _ = f _) - refine ⟨λ h => ?_, λ h => by { rw [r2, r3] ; congr }⟩ - suffices T (Γ₁ t) = T (Γ₂ t) by rw [← T.left_inv' l2, ← T.left_inv' l3] ; congr 1 - apply Prod.ext (by simpa [T.coe_fst, l2, l3]) - simpa using congr_arg Prod.snd (show (_, _) = (_, _) from (h ▸ r4).symm.trans r5) diff --git a/RMT4/Covering.lean b/RMT4/Covering.lean deleted file mode 100644 index 0724574..0000000 --- a/RMT4/Covering.lean +++ /dev/null @@ -1,240 +0,0 @@ -import RMT4.pintegral -import RMT4.LocallyConstant -import RMT4.to_mathlib -import RMT4.Bunch -import RMT4.Lift - -open Topology Filter Metric TopologicalSpace Set Subtype unitInterval - -variable {U : Set ℂ} {f : ℂ → ℂ} {Λ Λ' : LocalPrimitiveOn U f} - -namespace LocalPrimitiveOn - -variable {z w b1 : U} {u b2 w : ℂ} {a : U × ℂ} - -/-- The shift of `Λ.F z` going through a -/ -def FF (Λ : LocalPrimitiveOn U f) (z : U) (a : U × ℂ) (w : ℂ) : ℂ := Λ.F z w + (a.2 - Λ.F z a.1) - -@[simp] lemma FF_self {w : U} : Λ.FF z (w, u) w = u := by simp [FF] - -@[simp] lemma FF_self' {w : U × ℂ} : Λ.FF z w w.1 = w.2 := FF_self - -lemma FF_congr (h : Λ.FF z a b1 = b2) : Λ.FF z a = Λ.FF z (b1, b2) := by - rw [← h] ; unfold FF ; simp - -lemma FF_deriv (hw : w ∈ Λ.S z) : HasDerivAt (Λ.FF z a) (f w) w := Λ.der z w hw |>.add_const _ - -theorem isOpen_FF_eq (Λ Λ' : LocalPrimitiveOn U f) (i j : U × ℂ) (i1 j1 : U) : - IsOpen { z : U | z ∈ val ⁻¹' S Λ i1 ∩ val ⁻¹' S Λ' j1 ∧ Λ.FF i1 i ↑z = Λ'.FF j1 j ↑z } := by - simp only [isOpen_iff_nhds, mem_setOf_eq, nhds_induced, le_principal_iff, mem_comap, - preimage_subset_iff, Subtype.forall, and_imp] - rintro z _ ⟨h1, h2⟩ h3 - have l1 : ∀ᶠ w in 𝓝 z, HasDerivAt (Λ.FF i1 i) (f w) w := - eventually_of_mem (Λ.opn i1 |>.mem_nhds h1) (λ w => FF_deriv) - have l2 : ∀ᶠ w in 𝓝 z, HasDerivAt (Λ'.FF j1 j) (f w) w := - eventually_of_mem (Λ'.opn j1 |>.mem_nhds h2) (λ w => FF_deriv) - have l4 := @eventuallyEq_of_hasDeriv ℂ _ f (Λ.FF i1 i) (Λ'.FF j1 j) z l1 l2 h3 - have l5 := inter_mem (inter_mem l4 (Λ.opn i1 |>.mem_nhds h1)) (Λ'.opn j1 |>.mem_nhds h2) - exact ⟨_, l5, λ w _ h => ⟨⟨h.1.2, h.2⟩, h.1.1.symm⟩⟩ - -def toBunch (Λ : LocalPrimitiveOn U f) : Bunch (U × ℂ) U ℂ where - S i := val ⁻¹' Λ.S i.1 - F i w := Λ.FF i.1 i w - cmp _ _ := Λ.isOpen_FF_eq _ _ _ _ _ - -abbrev covering (Λ : LocalPrimitiveOn U f) := Λ.toBunch.space - -def map (Λ : LocalPrimitiveOn U f) (z : U) (w : U × ℂ) : covering Λ := (w.1, Λ.FF z (z, w.2) w.1) - -abbrev p (Λ : LocalPrimitiveOn U f) (z : covering Λ) : U := z.fst - -namespace covering - -variable {x a b : U} {s : Set (covering Λ)} - -/-- The shear transformation. `Φ z` maps a point `(u, v)` to `(u, w)` where `w` is the value above - `z` of the translate of `F z` that goes through `(u, v)`, and `(Φ z).symm` maps `(u, w)` to - `(u, v)` where `v` is the value above `u` of the translate of `F` that goes through `(z, v)`. -/ - -def Φ (Λ : LocalPrimitiveOn U f) (z : U) : covering Λ ≃ U × ℂ where - toFun w := (w.1, Λ.FF z w z) - invFun w := (w.1, Λ.FF z (z, w.2) w.1) - left_inv _ := by simp [FF] - right_inv _ := by simp [FF] - -def π (Λ : LocalPrimitiveOn U f) (z : U) : ℂ ≃ Λ.p ⁻¹' {z} where - toFun w := ⟨⟨z, w⟩, rfl⟩ - invFun w := w.val.2 - left_inv _ := rfl - right_inv := by rintro ⟨w, rfl⟩ ; rfl - -def ψ (Λ : LocalPrimitiveOn U f) (z : U) : U × ℂ ≃ U × Λ.p ⁻¹' {z} := - (Equiv.refl _).prodCongr (π Λ z) - -def Ψ (Λ : LocalPrimitiveOn U f) (z : U) : covering Λ ≃ U × Λ.p ⁻¹' {z} := - (Φ Λ z).trans (ψ Λ z) - -def L (Λ : LocalPrimitiveOn U f) (z : U) : PartialEquiv (covering Λ) (U × Λ.p ⁻¹' {z}) := - (Ψ Λ z).toPartialEquiv - -lemma L_image : (L Λ z).IsImage ((val ⁻¹' Λ.S z) ×ˢ univ) ((val ⁻¹' Λ.S z) ×ˢ univ) := by - intro ⟨z₁, z₂⟩ ; rw [mem_prod, mem_prod] ; simp [L, Ψ, ψ, Φ] - -def T_LocalEquiv (Λ : LocalPrimitiveOn U f) (z : U) : PartialEquiv (covering Λ) (U × Λ.p ⁻¹' {z}) := - L_image.restr - -def nhd_from (x : U) (z : covering Λ) : Filter (covering Λ) := - Filter.map (λ w => (w, Λ.FF x z w)) (𝓝 z.1) - -def nhd (z : covering Λ) : Filter (covering Λ) := nhd_from z.1 z - -lemma mem_nhd_from {z : covering Λ} : s ∈ nhd_from x z ↔ ∀ᶠ u in 𝓝 z.1, ⟨u, Λ.FF x z u⟩ ∈ s := - by rfl - -lemma titi1 {z : U × ℂ} (ha : z.1.1 ∈ Λ.S a) (hb : z.1.1 ∈ Λ'.S b) : - ∀ᶠ u in 𝓝 z.1, Λ.FF a z u = Λ'.FF b z u := by - -- let s := {z_1 : U | z_1 ∈ val ⁻¹' S Λ a ∩ val ⁻¹' S Λ' b ∧ FF Λ a z z_1 = FF Λ' b z z_1} - -- have e1 : IsOpen s := @isOpen_FF_eq U f Λ Λ' z z a b - -- have e2 : z.1 ∈ s := ⟨⟨ha, hb⟩, by simp only [FF_self']⟩ - -- have := e1.mem_nhds e2 - -- simp only [nhds_induced, mem_comap, preimage_subset_iff] at this - -- obtain ⟨t, ht1, ht2⟩ := this - -- apply eventually_of_mem ht1 - -- rintro x hx - let s := Λ.S a ∩ Λ'.S b - have l1 : IsOpen s := (Λ.opn a).inter (Λ'.opn b) - have l2 : s ∈ 𝓝 z.1.1 := l1.mem_nhds ⟨ha, hb⟩ - have l3 : LocallyConnectedSpace ℂ := by infer_instance - obtain ⟨t, ht1, ht2, ht3, ht4⟩ := locallyConnectedSpace_iff_open_connected_subsets.1 l3 z.1 s l2 - apply eventually_of_mem (ht2.mem_nhds ht3) - have l5 : ∀ x ∈ t, HasDerivAt (Λ.FF a z) (f x) x := λ x hx => Λ.FF_deriv (ht1 hx).1 - have l6 : ∀ x ∈ t, HasDerivAt (Λ'.FF b z) (f x) x := λ x hx => Λ'.FF_deriv (ht1 hx).2 - apply ht4.isPreconnected.apply_eq_of_hasDeriv_eq ht2 ht3 l5 l6 (by simp) - -lemma nhd_from_eq_nhd {z : covering Λ} (h : ↑z.1 ∈ Λ.S x) : nhd_from x z = nhd z := by - rw [nhd_from, nhd, nhd_from, nhds_induced] - apply Filter.map_congr - simp [EventuallyEq] - filter_upwards [titi1 h (Λ.mem z.1)] with w h1 w' h2 h3 - simp [h3, h1] - -lemma nhd_eq_toBunch_nhd : nhd = Λ.toBunch.nhd := by - ext ⟨a, b⟩ s - have : Nonempty (Λ.toBunch.idx (a, b)) := by - dsimp [toBunch, Bunch.idx, FF] - exact ⟨(a, b), Λ.mem a, by ring⟩ - simp only [Bunch.nhd, this, dite_true, IsBasis.mem_filter_iff] - constructor - · intro h - refine ⟨⟨(a, b), _⟩, ⟨?_, h⟩, ?_⟩ - · simpa [Bunch.reaches, Bunch.idx, toBunch] using Λ.mem a - · simpa [Bunch.tile] using subset_rfl - · rintro ⟨⟨z, t⟩, ⟨⟨h1, h2⟩, h3⟩, h4⟩ - simp only [← nhd_from_eq_nhd h1, nhd_from, mem_map] - apply mem_of_superset h3 - simp only [Bunch.tile] at h2 h4 - simpa [← Λ.FF_congr h2] using h4 - -lemma nhds_eq_nhd (z : covering Λ) : 𝓝 z = nhd z := by - simpa only [nhd_eq_toBunch_nhd] using Bunch.nhds_eq_nhd - -theorem isOpen_source (Λ : LocalPrimitiveOn U f) (z : ↑U) : - IsOpen (T_LocalEquiv Λ z).source := by - simp only [isOpen_iff_eventually, T_LocalEquiv, eventually_mem_set] - intro ⟨a₁, a₂⟩ ha - simp [L] at ha - rw [mem_prod] at ha ; simp at ha - simp only [nhds_eq_nhd, nhd, nhd_from, nhds_induced, mem_map, mem_comap] - refine ⟨Λ.S z, (Λ.opn z) |>.mem_nhds ha, ?_⟩ - exact λ x hx => by - simp at hx - simp [L] - rw [mem_prod] - simp [hx, map] - -theorem isOpen_target : IsOpen (T_LocalEquiv Λ z).target := by - simp [T_LocalEquiv, L] - exact IsOpen.prod (isOpen_induced (Λ.opn z)) isOpen_univ - -variable {α β : Type*} {s : Set (α × β)} {t : Set α} {b : β} - -lemma toto10 (l : Filter α) (b : β) : s ∈ l ×ˢ pure b ↔ ∃ t ∈ l, t ×ˢ {b} ⊆ s := by - simpa using exists_mem_subset_iff.symm - -lemma toto11 {s : Set (α × β)} : t ×ˢ {b} ⊆ s ↔ ∀ y ∈ t, (y, b) ∈ s where - mp h y hy := h ⟨hy, rfl⟩ - mpr h := by rintro ⟨y, b'⟩ ⟨hy, rfl⟩ ; exact h y hy - -lemma toto12 [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {s : Set (α × β)} - {w : α × β} : s ∈ 𝓝 w ↔ ∀ᶠ x in 𝓝 w.1, (x, w.2) ∈ s := by - rw [nhds_prod_eq, nhds_discrete β, toto10, eventually_iff_exists_mem] - simp only [toto11] - -lemma toto13 {s : Set (↑U × ↑(p Λ ⁻¹' {z}))} {w : U × Λ.p ⁻¹' {z}} : - s ∈ 𝓝 w ↔ ∀ᶠ x in 𝓝 w.1, (x, w.2) ∈ s := by - have l1 : DiscreteTopology (Λ.p ⁻¹' {z}) := Bunch.discreteTopology - exact toto12 - -theorem toto9 {w : covering Λ} (h : ↑w.1 ∈ Λ.S z) : ContinuousAt (T_LocalEquiv Λ z) w := by - rw [ContinuousAt, Tendsto] - intro s hs - rw [toto13] at hs - rw [nhds_eq_nhd, ← nhd_from_eq_nhd h] - simp [T_LocalEquiv, L, Ψ, ψ, π, Φ, mem_nhd_from] at hs ⊢ - filter_upwards [hs] with x hx - simpa [FF] using hx - -theorem toto9' {w : ↑U × ↑(p Λ ⁻¹' {z})} (h : ↑w.1 ∈ Λ.S z) : - ContinuousAt (T_LocalEquiv Λ z).symm w := by - rw [ContinuousAt, Tendsto] - intro s hs - simp - rw [toto13] - rw [nhds_eq_nhd, ← nhd_from_eq_nhd h] at hs - simp [T_LocalEquiv, L, Ψ, ψ, π, Φ, mem_nhd_from] at hs ⊢ - filter_upwards [hs] with x hx - simpa [FF] using hx - -theorem toto8 : ContinuousOn (T_LocalEquiv Λ z) (T_LocalEquiv Λ z).source := by - rintro w h - rw [continuousWithinAt_iff_continuousAt <| isOpen_source Λ z |>.mem_nhds h] - simp [T_LocalEquiv, L, Ψ, ψ, π, Φ] at h - rw [mem_prod] at h - simp only [mem_preimage, mem_univ, and_true] at h - apply toto9 h - -theorem toto8' : ContinuousOn (T_LocalEquiv Λ z).symm (T_LocalEquiv Λ z).target := by - rintro w h - rw [continuousWithinAt_iff_continuousAt <| isOpen_target |>.mem_nhds h] - simp only [T_LocalEquiv, L, PartialEquiv.IsImage.restr_target, Equiv.toPartialEquiv_target, - univ_inter, mem_prod, mem_preimage, mem_univ, and_true] at h - apply toto9' h - -def T_LocalHomeomorph (Λ : LocalPrimitiveOn U f) (z : U) : - PartialHomeomorph (covering Λ) (U × Λ.p ⁻¹' {z}) where - toPartialEquiv := T_LocalEquiv Λ z - open_source := isOpen_source Λ z - open_target := isOpen_target - continuousOn_toFun := toto8 - continuousOn_invFun := toto8' - -def T (Λ : LocalPrimitiveOn U f) (z : U) : Trivialization (Λ.p ⁻¹' {z}) (Λ.p) where - toPartialHomeomorph := T_LocalHomeomorph Λ z - baseSet := val ⁻¹' Λ.S z - open_baseSet := isOpen_induced (Λ.opn z) - source_eq := by simp [T_LocalHomeomorph, T_LocalEquiv, L] ; ext ; simp - target_eq := by simp [T_LocalHomeomorph, T_LocalEquiv, L] - proj_toFun x _:= rfl - -theorem isCoveringMap : IsCoveringMap (Λ.p) := - λ z => ⟨Bunch.discreteTopology, T Λ z, Λ.mem z⟩ - -end covering - -end LocalPrimitiveOn - -noncomputable def ContourIntegral (f : ℂ → ℂ) (Λ : LocalPrimitiveOn U f) (γ : C(I, U)) : ℂ := by - have l1 : IsCoveringMap Λ.p := LocalPrimitiveOn.covering.isCoveringMap - have l2 : γ 0 = Λ.p ⟨γ 0, 0⟩ := rfl - choose Γ _ _ using lift l1 l2 - exact (Γ 1).2 diff --git a/RMT4/Curvint.lean b/RMT4/Curvint.lean deleted file mode 100644 index 7be5aa7..0000000 --- a/RMT4/Curvint.lean +++ /dev/null @@ -1,202 +0,0 @@ -import RMT4.to_mathlib -import Mathlib.Topology.MetricSpace.Polish - -open intervalIntegral Real MeasureTheory Filter Topology Set Metric - -variable {a b t : ℝ} {γ : ℝ → ℂ} {i₀ w₀ : ℂ} {C : ℝ} - -section definitions - -/-- We start with a basic definition of the integral of a function along a path, which makes sense - when the path is differentiable -/ - -noncomputable def curvint (t₁ t₂ : ℝ) (f : ℂ → ℂ) (γ : ℝ → ℂ) : ℂ := - ∫ t in t₁..t₂, deriv γ t • f (γ t) - -/-- Version with `deriv_within` is useful -/ - -noncomputable def curvint' (t₁ t₂ : ℝ) (f : ℂ → ℂ) (γ : ℝ → ℂ) : ℂ := - ∫ t in t₁..t₂, derivWithin γ (Set.uIcc t₁ t₂) t • f (γ t) - -lemma curvint'_eq_curvint {f : ℂ → ℂ} {γ : ℝ → ℂ} : curvint' a b f γ = curvint a b f γ := - integral_congr_uIoo (λ _ ht => congr_arg₂ _ (derivWithin_of_mem_uIoo ht) rfl) - -end definitions - -section derivcurvint - -variable - {t₁ t₂ : ℝ} {F F' : ℂ → ℂ → ℂ} - -theorem hasDerivAt_curvint (ht : t₁ < t₂) - (γ_diff : ContDiffOn ℝ 1 γ (Icc t₁ t₂)) - (F_cont : ∀ᶠ i in 𝓝 i₀, ContinuousOn (F i) (γ '' Icc t₁ t₂)) - (F_deri : ∀ᶠ i in 𝓝 i₀, ∀ t ∈ Icc t₁ t₂, HasDerivAt (λ i => F i (γ t)) (F' i (γ t)) i) - (F'_cont : ContinuousOn (F' i₀) (γ '' Icc t₁ t₂)) - (F'_norm : ∀ᶠ i in 𝓝 i₀, ∀ t ∈ Icc t₁ t₂, ‖F' i (γ t)‖ ≤ C) - : - HasDerivAt (λ i => curvint t₁ t₂ (F i) γ) (curvint t₁ t₂ (F' i₀) γ) i₀ := by - simp_rw [← curvint'_eq_curvint] - set μ : Measure ℝ := volume.restrict (Ioc t₁ t₂) - set φ : ℂ → ℝ → ℂ := λ i t => derivWithin γ (Icc t₁ t₂) t • F i (γ t) - set ψ : ℂ → ℝ → ℂ := λ i t => derivWithin γ (Icc t₁ t₂) t • F' i (γ t) - obtain ⟨δ, hδ, h_in_δ⟩ := eventually_nhds_iff_ball.mp (F_deri.and F'_norm) - simp only [curvint'] - - have γ'_cont : ContinuousOn (derivWithin γ (Icc t₁ t₂)) (Icc t₁ t₂) := - γ_diff.continuousOn_derivWithin (uniqueDiffOn_Icc ht) le_rfl - obtain ⟨C', h⟩ := (isCompact_Icc.image_of_continuousOn γ'_cont).isBounded.subset_ball 0 - - have φ_cont : ∀ᶠ i in 𝓝 i₀, ContinuousOn (φ i) (Icc t₁ t₂) := by - filter_upwards [F_cont] with i h - exact γ'_cont.smul (h.comp γ_diff.continuousOn (mapsTo_image _ _)) - - have φ_meas : ∀ᶠ i in 𝓝 i₀, AEStronglyMeasurable (φ i) μ := by - filter_upwards [φ_cont] with i h - exact (h.mono Ioc_subset_Icc_self).aestronglyMeasurable measurableSet_Ioc - - have φ_intg : Integrable (φ i₀) μ := - φ_cont.self_of_nhds.integrableOn_Icc.mono_set Ioc_subset_Icc_self - - have φ_deri : ∀ᵐ t ∂μ, ∀ i ∈ ball i₀ δ, HasDerivAt (λ j => φ j t) (ψ i t) i := by - refine (ae_restrict_iff' measurableSet_Ioc).mpr (eventually_of_forall ?_) - intro t ht i hi - apply ((h_in_δ i hi).1 t (Ioc_subset_Icc_self ht)).const_smul - - have ψ_cont : ContinuousOn (ψ i₀) (Icc t₁ t₂) := - γ'_cont.smul (F'_cont.comp γ_diff.continuousOn (mapsTo_image _ _)) - - have ψ_meas : AEStronglyMeasurable (ψ i₀) μ := - (ψ_cont.mono Ioc_subset_Icc_self).aestronglyMeasurable measurableSet_Ioc - - have ψ_norm : ∀ᵐ t ∂μ, ∀ x ∈ ball i₀ δ, ‖ψ x t‖ ≤ C' * C := by - refine (ae_restrict_iff' measurableSet_Ioc).mpr (eventually_of_forall (λ t ht w hw => ?_)) - rw [norm_smul] - have e1 := mem_closedBall_zero_iff.mp $ - ball_subset_closedBall (h (mem_image_of_mem _ (Ioc_subset_Icc_self ht))) - have e2 := (h_in_δ w hw).2 t (Ioc_subset_Icc_self ht) - exact mul_le_mul e1 e2 (norm_nonneg _) ((norm_nonneg _).trans e1) - - have hC : Integrable (λ (_ : ℝ) => C' * C) μ := integrable_const _ - - simpa [curvint', intervalIntegral, ht.le] using - (hasDerivAt_integral_of_dominated_loc_of_deriv_le hδ φ_meas φ_intg ψ_meas ψ_norm hC φ_deri).2 - -end derivcurvint - -section bla - -variable {γ : ℝ → ℂ} {φ φ' : ℝ → ℝ} {f : ℂ → ℂ} - -theorem cdv - (φ_diff : ContDiffOn ℝ 1 φ (uIcc a b)) - (φ_maps : φ '' uIcc a b = uIcc (φ a) (φ b)) - (γ_diff : ContDiffOn ℝ 1 γ (uIcc (φ a) (φ b))) - (f_cont : ContinuousOn f (γ '' uIcc (φ a) (φ b))) - : - curvint (φ a) (φ b) f γ = curvint a b f (γ ∘ φ) := by - have l1 : ContinuousOn (fun x => derivWithin γ (uIcc (φ a) (φ b)) x • f (γ x)) (φ '' uIcc a b) := by - have e1 := γ_diff.continuousOn_derivWithin'' le_rfl - have e2 := f_cont.comp γ_diff.continuousOn (mapsTo_image _ _) - simpa only [φ_maps] using e1.smul e2 - simp_rw [← curvint'_eq_curvint, curvint', ← φ_diff.integral_derivWithin_smul_comp l1] - refine integral_congr_uIoo (λ t ht => ?_) - have l2 : MapsTo φ (uIcc a b) (uIcc (φ a) (φ b)) := φ_maps ▸ mapsTo_image _ _ - have l6 : t ∈ uIcc a b := uIoo_subset_uIcc ht - have l3 : DifferentiableWithinAt ℝ γ (uIcc (φ a) (φ b)) (φ t) := γ_diff.differentiableOn le_rfl (φ t) (l2 l6) - have l4 : DifferentiableWithinAt ℝ φ (uIcc a b) t := (φ_diff t l6).differentiableWithinAt le_rfl - have l5 : UniqueDiffWithinAt ℝ (uIcc a b) t := uniqueDiffWithinAt_of_mem_nhds (uIcc_mem_nhds ht) - simp [derivWithin.scomp t l3 l4 l2 l5] ; ring - -end bla - -namespace holo - -noncomputable def f1 (f : ℂ → ℂ) (Γ : ℂ → ℝ → ℂ) (w : ℂ) (t : ℝ) : ℂ := - deriv (Γ w) t * f (Γ w t) - -noncomputable def f2 (f f' : ℂ → ℂ) (Γ Γ' : ℂ → ℝ → ℂ) (w : ℂ) (t : ℝ) : ℂ := - deriv (Γ' w) t * f (Γ w t) + Γ' w t * deriv (Γ w) t * f' (Γ w t) - -noncomputable def f3 (f : ℂ → ℂ) (Γ Γ' : ℂ → ℝ → ℂ) (w : ℂ) (t : ℝ) : ℂ := - Γ' w t * f (Γ w t) - -/-- This gathers a lot of info that is enough to prove `holo.holo`, but it is a real mess and as - stated it is not clear that any non-constant function satisfies the assumptions. TODO: - - restrict to appropriate domains - - use `ContDiffOn` instead of separate assumptions - - actually prove `key` and `L` -/ - -structure setup (f f' : ℂ → ℂ) (Γ Γ' : ℂ → ℝ → ℂ) where - df : ∀ z, HasDerivAt f (f' z) z - cf' : Continuous f' - dΓ : ∀ w, Differentiable ℝ (Γ w) - dΓ' : ∀ w, Differentiable ℝ (Γ' w) - cdΓ : ∀ w, Continuous (deriv (Γ w)) - cdΓ' : ∀ w, Continuous (deriv (Γ' w)) - key : ∀ w t, HasDerivAt (fun w => f1 f Γ w t) (f2 f f' Γ Γ' w t) w - L : ∀ t, LipschitzOnWith (nnabs 1) (fun x => f1 f Γ x t) (ball w₀ 1) - -variable {f f' : ℂ → ℂ} {Γ Γ' : ℂ → ℝ → ℂ} - -lemma setup.cfΓ (S : setup (w₀ := w₀) f f' Γ Γ') (w : ℂ) : Continuous (f ∘ Γ w) := by - simpa [continuous_iff_continuousAt] - using λ t => (S.df (Γ w t)).continuousAt.comp (S.dΓ w t).continuousAt - -lemma setup.dfΓ (S : setup (w₀ := w₀) f f' Γ Γ') (w : ℂ) : Differentiable ℝ (λ t => f (Γ w t)) := by - intro t - apply ((S.df (Γ w t)).differentiableAt.restrictScalars ℝ).comp - exact (S.dΓ w t) - -lemma setup.continuous_f2 (S : setup (w₀ := w₀) f f' Γ Γ') (w : ℂ) : Continuous (f2 f f' Γ Γ' w) := by - unfold f2 - have := S.cf' - have := S.cdΓ w - have := S.cdΓ' w - have := (S.dfΓ w).continuous - have := (S.dΓ w).continuous - have := (S.dΓ' w).continuous - continuity - -variable {a b : ℝ} {f f' : ℂ → ℂ} {Γ Γ' : ℂ → ℝ → ℂ} - -theorem main_step (hab : a ≤ b) (S : setup (w₀ := w₀) f f' Γ Γ') : - HasDerivAt (fun w => ∫ (t : ℝ) in a..b, f1 f Γ w t) - (∫ (t : ℝ) in a..b, f2 f f' Γ Γ' w₀ t) w₀ := by - apply has_deriv_at_integral_of_continuous_of_lip (C := 1) hab -- or whatever - · exact zero_lt_one - · exact eventually_of_forall (λ z => ((S.cdΓ _).mul (S.cfΓ _)).continuousOn) - · exact λ _ _ => S.key _ _ - · exact λ _ _ => S.L _ - · exact (S.continuous_f2 w₀).continuousOn - -lemma identity (S : setup (w₀ := w₀) f f' Γ Γ') (w : ℂ) (t : ℝ) : - deriv (f3 f Γ Γ' w) t = f2 f f' Γ Γ' w t := by - unfold f2 f3 - rw [deriv_mul (S.dΓ' _).differentiableAt (S.dfΓ _).differentiableAt] - simp only [add_right_inj] - change Γ' w t * deriv (f ∘ Γ w) t = Γ' w t * deriv (Γ w) t * f' (Γ w t) - rw [← (S.df (Γ w t)).deriv, deriv.comp _ (S.df _).differentiableAt (S.dΓ _).differentiableAt] - ring - -theorem holo (hab : a ≤ b) (S : setup (w₀ := w₀) f f' Γ Γ') : - HasDerivAt (fun w => curvint a b f (Γ w)) - (Γ' w₀ b * f (Γ w₀ b) - Γ' w₀ a * f (Γ w₀ a)) w₀ := by - have : HasDerivAt (fun w => ∫ (t : ℝ) in a..b, f1 f Γ w t) - (∫ (t : ℝ) in a..b, f2 f f' Γ Γ' w₀ t) w₀ := main_step hab S - convert ← this - simp only [← identity S] - unfold f3 - apply intervalIntegral.integral_deriv_eq_sub' _ rfl - · intro t _ - apply (S.dΓ' _).mul - have := S.dfΓ w₀ - exact S.dfΓ _ - · apply Continuous.continuousOn - have : deriv (fun t => Γ' w₀ t * f (Γ w₀ t)) = - (λ t => deriv (Γ' w₀) t * f (Γ w₀ t) + Γ' w₀ t * deriv (Γ w₀) t * f' (Γ w₀ t)) := by - ext1 t ; exact identity S w₀ t - rw [this] - exact S.continuous_f2 w₀ - -end holo diff --git a/RMT4/Glue.lean b/RMT4/Glue.lean deleted file mode 100644 index 1c0bef5..0000000 --- a/RMT4/Glue.lean +++ /dev/null @@ -1,120 +0,0 @@ -import Mathlib.Topology.ContinuousFunction.Basic -import Mathlib.Topology.MetricSpace.PseudoMetric -import Mathlib.Topology.Algebra.Order.ProjIcc - -open Set Interval - -variable {a b c t : ℝ} {E : Type*} [TopologicalSpace E] - -section real - -variable {f g : ℝ → E} - -noncomputable def glue_at (b : ℝ) (f g : ℝ → E) := λ t => if t ≤ b then f t else g t - -lemma continuous_glue (hf : Continuous f) (hg : Continuous g) (h : f b = g b) : - Continuous (glue_at b f g) := - hf.if_le hg continuous_id continuous_const (λ _ hx => hx.symm ▸ h) - -end real - -section Icc - -variable {F : Icc a b → E} {G : Icc b c → E} - -noncomputable def glue_Icc (F : Icc a b → E) (G : Icc b c → E) (t : Icc a c) : E := - if h : t ≤ b then F ⟨t, t.2.1, h⟩ else G ⟨t, not_le.1 h |>.le, t.2.2⟩ - -lemma glue_Icc_eq (hab : a ≤ b) (hbc : b ≤ c) : - glue_Icc F G = λ t : Icc a c => if t ≤ b then IccExtend hab F t else IccExtend hbc G t := by - ext t ; simp [glue_Icc] ; split_ifs <;> symm <;> apply IccExtend_of_mem - -lemma continuous_glue_Icc (hF : Continuous F) (hG : Continuous G) (hab : a ≤ b) (hbc : b ≤ c) - (h : F ⟨b, right_mem_Icc.2 hab⟩ = G ⟨b, left_mem_Icc.2 hbc⟩) : - Continuous (glue_Icc F G) := by - rw [glue_Icc_eq hab hbc] - exact continuous_glue hF.Icc_extend' hG.Icc_extend' (by simpa) |>.comp continuous_subtype_val - -noncomputable def ContinuousMap.trans (hab : a ≤ b) (hbc : b ≤ c) (F : C(Icc a b, E)) - (G : C(Icc b c, E)) (h : F ⟨b, right_mem_Icc.2 hab⟩ = G ⟨b, left_mem_Icc.2 hbc⟩) : - C(Icc a c, E) where - toFun := glue_Icc F G - continuous_toFun := continuous_glue_Icc F.continuous G.continuous hab hbc h - -end Icc - -section uIcc - -variable {F : Icc a b → E} {G : uIcc b c → E} - -noncomputable def glue_uIcc (F : Icc a b → E) (G : uIcc b c → E) (t : Icc a c) : E := - if h : t ≤ b then F ⟨t, t.2.1, h⟩ else - G ⟨t, inf_le_left.trans <| not_le.1 h |>.le, t.2.2.trans le_sup_right⟩ - -@[simp] lemma glue_uIcc_left (hab : a ≤ b) (hac : a ≤ c) : - glue_uIcc F G ⟨a, left_mem_Icc.2 hac⟩ = F ⟨a, left_mem_Icc.2 hab⟩ := by - simp [glue_uIcc, hab] - -lemma glue_uIcc_eq (hab : a ≤ b) : glue_uIcc F G = λ t : Icc a c => - if t ≤ b then IccExtend hab F t else IccExtend inf_le_sup G t := by - ext t ; simp [glue_uIcc] ; split_ifs <;> symm <;> apply IccExtend_of_mem - -lemma continuous_glue_uIcc (hF : Continuous F) (hG : Continuous G) (hab : a ≤ b) - (h : F ⟨b, right_mem_Icc.2 hab⟩ = G ⟨b, left_mem_uIcc⟩) : Continuous (glue_uIcc F G) := by - rw [glue_uIcc_eq hab] - suffices Continuous fun t => if t ≤ b then IccExtend hab F t else IccExtend inf_le_sup G t from - this.comp continuous_subtype_val - refine hF.Icc_extend'.if_le hG.Icc_extend' continuous_id continuous_const (λ x hx => ?_) - simpa [IccExtend_of_mem, hx] using h - -noncomputable def ContinuousMap.trans' (hab : a ≤ b) (F : C(Icc a b, E)) (G : C(uIcc b c, E)) - (h : F ⟨b, right_mem_Icc.2 hab⟩ = G ⟨b, left_mem_uIcc⟩) : C(Icc a c, E) where - toFun := glue_uIcc F G - continuous_toFun := continuous_glue_uIcc F.continuous G.continuous hab h - -@[simp] lemma ContinuousMap.trans'_left (hab : a ≤ b) (hac : a ≤ c) {F : C(Icc a b, E)} - {G : C(uIcc b c, E)} (h : F ⟨b, right_mem_Icc.2 hab⟩ = G ⟨b, left_mem_uIcc⟩) : - F.trans' hab G h ⟨a, left_mem_Icc.2 hac⟩ = F ⟨a, left_mem_Icc.2 hab⟩ := by - simp [ContinuousMap.trans', hab, hac] - -end uIcc - -section Iic - -variable - {T E : Type*} [LinearOrder T] [TopologicalSpace T] [OrderTopology T][OrderClosedTopology T] {a b : T} - {E : Type*} [TopologicalSpace E] {f : Iic a → E} {g : uIcc a b → E} - -def glue_Iic (f : Iic a → E) (g : uIcc a b → E) (t : Iic b) : E := - if h : t ≤ a then f ⟨t, h⟩ else g ⟨t, inf_le_left.trans (not_le.1 h).le, t.2.trans le_sup_right⟩ - -lemma glue_Iic_eq : glue_Iic f g = λ t : Iic b => - if t ≤ a then IicExtend f t else IccExtend inf_le_sup g t := by - ext t ; simp [glue_Iic] ; split_ifs <;> symm - · apply IicExtend_of_mem - · apply IccExtend_of_mem - -lemma continuous_projIic : Continuous (Set.projIic a) := - (continuous_const.min continuous_id).subtype_mk _ - -lemma Continuous.Iic_extend' (hf : Continuous f) : Continuous (IicExtend f) := - hf.comp continuous_projIic - -lemma continuous_glue_Iic (hf : Continuous f) (hg : Continuous g) - (h : f ⟨a, le_rfl⟩ = g ⟨a, ⟨inf_le_left, le_sup_left⟩⟩) : Continuous (glue_Iic f g) := by - rw [glue_Iic_eq] - suffices h : Continuous fun t => if t ≤ a then IicExtend f t else IccExtend inf_le_sup g t - by exact h.comp continuous_subtype_val - refine hf.Iic_extend'.if_le hg.Icc_extend' continuous_id continuous_const ?_ - rintro x rfl ; simpa [IccExtend_of_mem] using h - -def ContinuousMap.trans_Iic (F : C(Iic a, E)) (G : C(uIcc a b, E)) - (h : F ⟨a, le_rfl⟩ = G ⟨a, ⟨inf_le_left, le_sup_left⟩⟩) : C(Iic b, E) := - ⟨glue_Iic F G, continuous_glue_Iic F.continuous G.continuous h⟩ - -@[simp] lemma ContinuousMap.trans_Iic_of_le {F : C(Iic a, E)} {G : C(uIcc a b, E)} - {h : F ⟨a, le_rfl⟩ = G ⟨a, ⟨inf_le_left, le_sup_left⟩⟩} {u : Iic b} (hu : u ≤ a) : - F.trans_Iic G h u = F ⟨u, hu⟩ := by - simp [trans_Iic, glue_Iic, hu] - -end Iic diff --git a/RMT4/Lift.lean b/RMT4/Lift.lean deleted file mode 100644 index 4b444c5..0000000 --- a/RMT4/Lift.lean +++ /dev/null @@ -1,196 +0,0 @@ -import Mathlib.Analysis.Convex.Normed -import Mathlib.Analysis.Convex.Segment -import Mathlib.Topology.Covering -import Mathlib.Topology.LocallyConstant.Basic -import RMT4.Glue -import Mathlib - -open Set Topology Metric unitInterval Filter ContinuousMap - -variable {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} - -section Lift - -variable {γ : C(I, X)} {x : X} {A : E} {t t₁ t₂ : I} {Γ Γ₁ Γ₂ : C(I, E)} - -lemma isClopen_iff_nhds {E : Type*} [TopologicalSpace E] {s : Set E} : - IsClopen s ↔ ∀ a, ∀ᶠ b in 𝓝 a, b ∈ s ↔ a ∈ s where - mp h a := by - by_cases h3 : a ∈ s - · simpa [h3] using h.2.mem_nhds h3 - · simpa only [h3, iff_false] using h.1.isOpen_compl.mem_nhds h3 - mpr h := by - constructor - · exact ⟨by simpa [isOpen_iff_mem_nhds] using λ a ha => by simpa only [ha, iff_false] using h a⟩ - · simpa [isOpen_iff_mem_nhds] using λ a ha => by simpa [ha] using h a - -instance : Zero (Iic t) := ⟨0, nonneg'⟩ --- instance : ZeroLEOneClass I := ⟨nonneg'⟩ - -def reachable (f : E → X) (γ : C(I, X)) (A : E) (t : I) : Prop := - ∃ Γ : C(Iic t, E), Γ 0 = A ∧ ∀ s, f (Γ s) = γ s - -def reachable' (f : E → X) (γ : C(I, X)) (A : E) (t : I) : Prop := - ∃ Γ : C(I, E), Γ 0 = A ∧ ∀ s ≤ t, f (Γ s) = γ s - -example : reachable f γ A t ↔ reachable' f γ A t := by - constructor - · rintro ⟨Γ, h1, h2⟩ - refine ⟨⟨IicExtend Γ, ?_⟩, ?_, ?_⟩ - · apply Continuous.comp Γ.2 - apply Continuous.subtype_mk - apply continuous_const.min continuous_id - · simp [IicExtend, projIic, min, ← h1] - congr - simp [inf_eq_right, t.2.1] - · intro s hs - specialize h2 ⟨s, hs⟩ - simp at h2 - simp [← h2, IicExtend, projIic, min_eq_right hs] - · sorry - -lemma reachable_zero (hγ : γ 0 = f A) : reachable f γ A 0 := by - refine ⟨⟨λ _ => A, continuous_const⟩, rfl, ?_⟩ - intro ⟨s, (hs : s ≤ 0)⟩ ; simp [le_antisymm hs s.2.1, hγ] - -lemma reachable_extend {T : Trivialization (f ⁻¹' {γ t}) f} (h : MapsTo γ (uIcc t₁ t₂) T.baseSet) : - reachable f γ A t₁ → reachable f γ A t₂ := by - rintro ⟨Γ, rfl, h2⟩ - let T₁ : Iic t₁ := ⟨t₁, mem_Iic.2 le_rfl⟩ - let δ : C(uIcc t₁ t₂, E) := ⟨λ s => T.invFun ⟨γ s, (T (Γ T₁)).2⟩, - T.continuousOn_invFun.comp_continuous (by continuity) (λ t => by simp only [T.mem_target, h t.2])⟩ - have l1 : f (Γ T₁) = γ t₁ := h2 T₁ - have l2 : Γ T₁ ∈ T.source := T.mem_source.2 <| l1 ▸ h left_mem_uIcc - refine ⟨trans_Iic Γ δ ?_, trans_Iic_of_le nonneg', λ s => ?_⟩ - · simpa only [T₁, δ, ContinuousMap.coe_mk, ← l1, ← T.proj_toFun _ l2] using (T.left_inv' l2).symm - · by_cases H : s ≤ t₁ <;> simp only [trans_Iic, glue_Iic, ContinuousMap.coe_mk, H, dite_true, h2] - have l5 : γ s ∈ T.baseSet := h ⟨inf_le_left.trans (not_le.1 H).le, le_trans s.2 le_sup_right⟩ - have l6 {z} : (γ s, z) ∈ T.target := T.mem_target.2 l5 - exact (T.proj_toFun _ (T.map_target' l6)).symm.trans <| congr_arg Prod.fst (T.right_inv' l6) - -lemma reachable_nhds_iff (hf : IsCoveringMap f) : - ∀ᶠ t' in 𝓝 t, (reachable f γ A t' ↔ reachable f γ A t) := by - obtain ⟨_, T, h4⟩ := hf (γ t) - have l2 := γ.continuousAt _ |>.preimage_mem_nhds <| T.open_baseSet.mem_nhds h4 - simp only [Filter.Eventually, Metric.mem_nhds_iff] at l2 ⊢ - obtain ⟨ε, hε, l3⟩ := l2 - refine ⟨ε, hε, λ u hu => ?_⟩ - have : segment ℝ t.1 u.1 ⊆ ball t.1 ε := (convex_ball t.1 ε).segment_subset (mem_ball_self hε) hu - have l5 : uIcc t.1 u.1 ⊆ ball t.1 ε := by rwa [← segment_eq_uIcc] - have l6 : MapsTo γ (uIcc t u) T.baseSet := λ v hv => l3 (l5 hv) - exact ⟨reachable_extend <| uIcc_comm t u ▸ l6, reachable_extend l6⟩ - -theorem IsCoveringMap.eq_of_comp_eq' (hf : IsCoveringMap f) {A : Type*} [TopologicalSpace A] - [PreconnectedSpace A] {g₁ g₂ : C(A, E)} (he : f ∘ g₁ = f ∘ g₂) (a : A) (ha : g₁ a = g₂ a) : - g₁ = g₂ := - ContinuousMap.ext (congrFun <| hf.eq_of_comp_eq g₁.continuous_toFun g₂.continuous_toFun he a ha) - -theorem lift_unique (hf : IsCoveringMap f) {Γ₁ Γ₂ : C(I, E)} (h0 : Γ₁ 0 = Γ₂ 0) - (h : f ∘ Γ₁ = f ∘ Γ₂) : Γ₁ = Γ₂ := by - exact hf.eq_of_comp_eq' h 0 h0 - -theorem Lift (hf : IsCoveringMap f) (hγ : γ 0 = f A) : ∃! Γ : C(I, E), Γ 0 = A ∧ f ∘ Γ = γ := by - have l1 : Set.Nonempty {t | reachable f γ A t} := ⟨0, reachable_zero hγ⟩ - have l2 : IsClopen {t | reachable f γ A t} := isClopen_iff_nhds.2 (λ t => reachable_nhds_iff hf) - let ⟨Γ, h1, h2⟩ := ((isClopen_iff.1 l2).resolve_left <| Nonempty.ne_empty l1).symm ▸ mem_univ 1 - let Γ₁ : C(I, E) := ⟨IicExtend Γ, Γ.2.Iic_extend'⟩ - have l3 : Γ₁ 0 = A := by simpa [Γ₁, IicExtend, projIic] using h1 - have l4 : f ∘ Γ₁ = γ := by - ext1 s - simp only [IicExtend, coe_mk, Function.comp_apply, projIic] - convert h2 ⟨s, s.2.2⟩ - simp [Γ₁, IicExtend, projIic] - congr - simpa using s.2.2 - refine ⟨Γ₁, ⟨l3, l4⟩, ?_⟩ - intro Γ₂ ⟨hh1, hh2⟩ - exact hf.eq_of_comp_eq' (l4 ▸ hh2) 0 (l3 ▸ hh1) - -theorem lift (hf : IsCoveringMap f) (hγ : γ 0 = f A) : ∃ Γ : C(I, E), Γ 0 = A ∧ f ∘ Γ = γ := - (Lift hf hγ).exists - -end Lift - -namespace HomotopyLift - -variable {γ : C(I × I, X)} {e : E} {Y : Type*} [TopologicalSpace Y] [LocallyConnectedSpace Y] - {p : E → X} - -instance : LocallyConnectedSpace I := sorry - -instance : LocPathConnectedSpace I := sorry - --- Consider $y_0 ∈ Y$. For any $t$, $F(y_0, t)$ has an evenly covered neighbourhood $U_t$ in $X$. --- By compactness of $\{y0\} × I$, we may take finitely many intervals {J_i} that cover I and a --- path-connected neighbourhood V of y0 so that, for each i, F(V × J_i) is contained in some --- evenly covered set U_i. -lemma lemma1 {y₀} {F : C(Y × ↑I, X)} {T : (t : I) → Trivialization (p ⁻¹' {F (y₀, t)}) p} - (hT : ∀ t, F (y₀, t) ∈ (T t).baseSet) : ∃ V ∈ 𝓝 y₀, ∃ S : Finset I, ∃ J : I → Set I, - IsConnected V ∧ (∀ s ∈ S, IsConnected (J s) ∧ ⇑F '' V ×ˢ J s ⊆ (T s).baseSet) ∧ - ⋃ s ∈ S, J s = univ := by - let W t : Set (Y × I) := F ⁻¹' (T t).baseSet - have h1 t : ∃ V ∈ 𝓝 y₀, ∃ J ∈ 𝓝 t, IsConnected J ∧ V ×ˢ J ⊆ W t := by - have l1 : IsOpen (W t) := (T t).open_baseSet.preimage F.continuous_toFun - obtain ⟨V, hV, J₀, hJ₀, h⟩ := mem_nhds_prod_iff.mp <| l1.mem_nhds (hT _) - obtain ⟨J, hJ1, hJ2, hJ3⟩ := locallyConnectedSpace_iff_connected_subsets.mp inferInstance _ _ hJ₀ - exact ⟨V, hV, J, hJ1, ⟨⟨t, mem_of_mem_nhds hJ1⟩, hJ2⟩, subset_trans (Set.prod_mono_right hJ3) h⟩ - choose Vt hV J hJ hJ2 hVJ using h1 - choose S hS using CompactSpace.elim_nhds_subcover J hJ - have h2 : ⋂ s ∈ S, Vt s ∈ 𝓝 y₀ := (Filter.biInter_finset_mem _).mpr (λ s _ => hV s) - have h3 := locallyConnectedSpace_iff_connected_subsets.mp inferInstance y₀ _ h2 - obtain ⟨V, hV1, hV2, hV3⟩ := h3 - refine ⟨V, hV1, S, J, ⟨⟨y₀, mem_of_mem_nhds hV1⟩, hV2⟩, λ s hs => ⟨hJ2 s, ?_⟩, hS⟩ - refine image_subset_iff.mpr (subset_trans ?_ (hVJ s)) - exact Set.prod_mono_left <| hV3.trans <| biInter_subset_of_mem hs - -theorem HLL (hp : IsCoveringMap p) (f₀ : C(Y, X)) (F : C(Y × I, X)) (hF : ∀ y, F (y, 0) = f₀ y) - (g₀ : Y → E) (hg₀ : p ∘ g₀ = f₀) : ∃! G : C(Y × I, E), p ∘ G = F ∧ ∀ y, G (y, 0) = g₀ y := by - let γ : C(Y, C(I, X)) := F.curry - have h1 {y} : γ y 0 = f₀ y := hF y - have h3 {y} : γ y 0 = p (g₀ y) := by rw [h1, ← congr_fun hg₀ y] ; rfl - choose G hG1 hG2 using λ y => @Lift _ _ _ _ _ (γ y) (g₀ y) hp h3 - - have h4 (y₀ : Y) (t : I) := (hp (F (y₀, t))).2 - choose T hT using h4 - let U y₀ t := (T y₀ t).baseSet - - have step1 y₀ : ∃ V ∈ 𝓝 y₀, ∃ S : Finset I, ∃ J : I → Set I, IsConnected V ∧ - (∀ s ∈ S, IsConnected (J s) ∧ F '' (V ×ˢ J s) ⊆ U y₀ s) ∧ (⋃ s ∈ S, J s = univ) := - lemma1 (hT y₀) - choose! V hV S J h using step1 - - - -- Let $U_{δ_i}$ be the unique slice of p^{−1}(U_i) such that $\hat F({y0} × J_i) ⊆ U_{δ_i}$. - - refine ⟨⟨λ yt => G yt.1 yt.2, ?_⟩, ⟨?_, ?_⟩, ?_⟩ - · rw [continuous_iff_continuousAt] - intro yt - obtain ⟨T, hT⟩ := (hp (f (g₀ yt.1))).2 - sorry - · exact funext (λ yt => congr_fun (hG1 yt.1).2 yt.2) - · exact λ y => (hG1 y).1 - · intro H ⟨hH1, hH2⟩ - ext ⟨y, t⟩ - let Hy : C(I, E) := ⟨λ t => H (y, t), sorry⟩ - have h4 : (p ∘ fun t => H (y, t)) = fun t => F (y, t) := sorry - simp [← hG2 y Hy ⟨hH2 y, h4⟩, Hy] - --- theorem HomLift (hf : IsCoveringMap f) (h0 : γ (0, 0) = f e) : --- ∃ Γ : C(I × I, E), Γ (0, 0) = e ∧ f ∘ Γ = γ := by --- -- track starting points --- let φ : C(I, I × I) := ⟨λ s => (s, 0), continuous_prod_mk.mpr ⟨continuous_id, continuous_const⟩⟩ --- let ζ : C(I, X) := γ.comp φ --- obtain ⟨Z, ⟨hZ1, hZ2⟩, hZ3⟩ := lift' (γ := ζ) hf h0 --- -- build layers --- let ψ s : C(I, I × I) := ⟨λ t => (s, t), continuous_prod_mk.mpr ⟨continuous_const, continuous_id⟩⟩ --- let δ s : C(I, X) := γ.comp (ψ s) --- have l1 {s} : (δ s) 0 = f (Z s) := (congr_fun hZ2 s).symm --- choose Δ hΔ1 hΔ2 using λ s => @lift' E X _ _ f (δ s) (Z s) hf l1 --- -- finish proof --- refine ⟨⟨λ st => Δ st.1 st.2, ?_⟩, ?_, ?_⟩ --- · --- sorry --- · simp [(hΔ1 0).1, hZ1] --- · exact funext <| λ st => congr_fun (hΔ1 st.1).2 st.2 - -end HomotopyLift diff --git a/RMT4/LocallyConstant.lean b/RMT4/LocallyConstant.lean deleted file mode 100644 index 6488b57..0000000 --- a/RMT4/LocallyConstant.lean +++ /dev/null @@ -1,65 +0,0 @@ -import Mathlib.Tactic -import Mathlib.Analysis.Calculus.Deriv.Basic -import Mathlib.Analysis.Calculus.MeanValue -import Mathlib.Topology.LocallyConstant.Basic - -open Topology Filter Metric - -variable {𝕜 : Type*} [IsROrC 𝕜] {f f₁ f₂ F1 F2 : 𝕜 → 𝕜} {z z₀ : 𝕜} {s : Set 𝕜} {U : Set 𝕜} - -lemma isConst_nhds_of_hasDerivAt (h : ∀ᶠ w in 𝓝 z, HasDerivAt f 0 w) : ∀ᶠ w in 𝓝 z, f w = f z := by - obtain ⟨r, hr, hf⟩ := eventually_nhds_iff_ball.1 h - refine eventually_nhds_iff_ball.2 ⟨r, hr, λ w hw => ?_⟩ - have l1 : DifferentiableOn 𝕜 f (ball z r) := - λ w hw => (hf w hw).differentiableAt.differentiableWithinAt - have l2 (w) (hw : w ∈ ball z r) : fderivWithin 𝕜 f (ball z r) w = 0 := by - have l3 : UniqueDiffWithinAt 𝕜 (ball z r) w := isOpen_ball.uniqueDiffWithinAt hw - have l4 := (hf w hw).hasFDerivAt.hasFDerivWithinAt.fderivWithin l3 - rw [l4] ; ext1 ; simp - exact (convex_ball z r).is_const_of_fderivWithin_eq_zero l1 l2 hw (mem_ball_self hr) - -lemma eventuallyEq_of_hasDeriv' (h1 : ∀ᶠ w in 𝓝 z, HasDerivAt F1 (f w) w) - (h2 : ∀ᶠ w in 𝓝 z, HasDerivAt F2 (f w) w) : ∀ᶠ w in 𝓝 z, F2 w - F2 z = F1 w - F1 z := by - have : ∀ᶠ w in 𝓝 z, HasDerivAt (F2 - F1) 0 w := by - filter_upwards [h1, h2] with w h1 h2 ; simpa using h2.sub h1 - filter_upwards [isConst_nhds_of_hasDerivAt this] with w h - simpa [sub_eq_sub_iff_sub_eq_sub] using h - -lemma eventuallyEq_of_hasDeriv (h1 : ∀ᶠ w in 𝓝 z, HasDerivAt F1 (f w) w) - (h2 : ∀ᶠ w in 𝓝 z, HasDerivAt F2 (f w) w) (h3 : F1 z = F2 z) : ∀ᶠ w in 𝓝 z, F2 w = F1 w := by - filter_upwards [eventuallyEq_of_hasDeriv' h1 h2] with a ha - simpa [h3, sub_left_inj] using ha - -lemma isLocallyConstant_of_deriv_eq_zero (hU : IsOpen U) (h : DifferentiableOn 𝕜 f U) - (hf : U.EqOn (deriv f) 0) : - IsLocallyConstant (U.restrict f) := by - refine (IsLocallyConstant.iff_exists_open _).2 (λ ⟨z, hz⟩ => ?_) - obtain ⟨ε, L1, L2⟩ := isOpen_iff.1 hU z hz - refine ⟨ball ⟨z, hz⟩ ε, isOpen_ball, mem_ball_self L1, λ ⟨z', _⟩ hz' => ?_⟩ - refine (convex_ball z ε).is_const_of_fderivWithin_eq_zero (h.mono L2) ?_ hz' (mem_ball_self L1) - intro x hx - rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hx)] - · exact ContinuousLinearMap.ext_ring (hf (L2 hx)) - · exact h.differentiableAt (hU.mem_nhds (L2 hx)) - -lemma isLocallyConstant_of_hasDeriv (hs : IsOpen s) (hf : ∀ x ∈ s, HasDerivAt f 0 x) : - IsLocallyConstant (s.restrict f) := by - apply isLocallyConstant_of_deriv_eq_zero hs - · exact λ x hx => (hf x hx).differentiableAt.differentiableWithinAt - · exact λ x hx => (hf x hx).deriv - -lemma IsPreconnected.apply_eq_of_hasDeriv_zero (hs : IsOpen s) (hs' : IsPreconnected s) - (hf : ∀ x ∈ s, HasDerivAt f 0 x) : ∀ x ∈ s, ∀ y ∈ s, f x = f y := by - have l0 : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.1 hs' - have l1 := isLocallyConstant_of_hasDeriv hs hf - have l2 : IsPreconnected (Set.univ : Set s) := preconnectedSpace_iff_univ.mp l0 - intro x hx y hy - simpa using - l1.apply_eq_of_isPreconnected l2 (x := ⟨x, hx⟩) (y := ⟨y, hy⟩) (Set.mem_univ _) (Set.mem_univ _) - -lemma IsPreconnected.apply_eq_of_hasDeriv_eq (hs' : IsPreconnected s) (hs : IsOpen s) (hz₀ : z₀ ∈ s) - (hf₁ : ∀ x ∈ s, HasDerivAt f₁ (f x) x) (hf₂ : ∀ x ∈ s, HasDerivAt f₂ (f x) x) - (h : f₁ z₀ = f₂ z₀) : Set.EqOn f₁ f₂ s := by - have l1 (x) (hx : x ∈ s) : HasDerivAt (f₁ - f₂) 0 x := by simpa using (hf₁ x hx).sub (hf₂ x hx) - intro x hx - simpa [h, sub_eq_zero] using hs'.apply_eq_of_hasDeriv_zero hs l1 x hx z₀ hz₀ diff --git a/RMT4/Primitive.lean b/RMT4/Primitive.lean deleted file mode 100644 index 88b0b0f..0000000 --- a/RMT4/Primitive.lean +++ /dev/null @@ -1,132 +0,0 @@ -import RMT4.to_mathlib -import Mathlib.Order.Interval - -open Set BigOperators Metric Filter MeasureTheory intervalIntegral - -variable {f : ℂ → ℂ} {z₀ z w : ℂ} {ε δ t a b : ℝ} {K U : Set ℂ} - -lemma mem_segment (ht : t ∈ Icc (0 : ℝ) 1) : (1 - t) • z₀ + t • z ∈ segment ℝ z₀ z := - ⟨1 - t, t, by linarith [ht.2], ht.1, by ring, rfl⟩ - -lemma continuous_bary : Continuous (λ t : ℝ => (1 - t) • z₀ + t • z) := by continuity - -lemma differentiable_bary : Differentiable ℂ (λ z : ℂ => (1 - t) • z₀ + t • z) := - (differentiable_const _).add (differentiable_id.const_smul _) - -lemma has_deriv_at_bary : HasDerivAt (λ t : ℝ => (1 - t) • z₀ + t • z) (z - z₀) t := by - have h0 : HasDerivAt (1 - ·) (-1) t := by - simpa using (hasDerivAt_const t 1).sub (hasDerivAt_id t) - have h1 : HasDerivAt (λ t : ℝ => (1 - t) • z₀) (-z₀) t := by - simpa using h0.smul_const z₀ - have h2 : HasDerivAt (· • z) z t := by - simpa using (hasDerivAt_id t).smul_const z - convert h1.add h2 using 1 ; ring - -lemma hasDerivAt_bary' : HasDerivAt (λ z => (1 - t) • z₀ + t • z) t z := by - simpa using (hasDerivAt_const z ((1 - t) • z₀)).add ((hasDerivAt_id z).const_smul t) - -lemma StarConvex.bary (hU : StarConvex ℝ z₀ U) (hz : z ∈ U) : - MapsTo (λ t : ℝ => (1 - t) • z₀ + t • z) (Icc 0 1) U := - λ _ ht => hU.segment_subset hz (mem_segment ht) - -noncomputable def primitive (f : ℂ → ℂ) (z₀ z : ℂ) : ℂ := - (z - z₀) * ∫ t in (0:ℝ)..1, f ((1 - t) • z₀ + t • z) - --- lemma primitive_eq_curvint : primitive f z₀ z = curvint 0 1 f (λ t, (1 - t) • z₀ + t • z) := --- by simpa only [curvint, has_deriv_at_bary.deriv] --- using (interval_integral.integral_const_mul _ _).symm - -namespace detail - -noncomputable abbrev φ (f : ℂ → ℂ) (z₀ z : ℂ) (t : ℝ) : ℂ := f ((1 - t) • z₀ + t • z) - -noncomputable abbrev ψ (f : ℂ → ℂ) (z₀ z : ℂ) (t : ℝ) : ℂ := t • deriv f ((1 - t) • z₀ + t • z) - -end detail - -open detail - -lemma DifferentiableOn.exists_primitive (f_holo : DifferentiableOn ℂ f U) - (hU : StarConvex ℝ z₀ U) (hU' : IsOpen U) (hz : z ∈ U) : - HasDerivAt (primitive f z₀) (f z) z := by - - let φ := φ f z₀ - let ψ := ψ f z₀ - let I : Set ℝ := Icc 0 1 - - have f_cont : ContinuousOn f U := f_holo.continuousOn - have f_deri : ∀ ⦃z⦄ (_ : z ∈ U), HasDerivAt f (_root_.deriv f z) z := - λ z hz => f_holo.hasDerivAt (hU'.mem_nhds hz) - have f_cder : ContinuousOn (_root_.deriv f) U := (f_holo.analyticOn hU').deriv.continuousOn - - have φ_cont {z} (hz : z ∈ U) : ContinuousOn (φ z) I := - f_cont.comp continuous_bary.continuousOn (hU.bary hz) - have φ_diff {t} (ht : t ∈ I) : DifferentiableOn ℂ (λ w => φ w t) U := - f_holo.comp differentiable_bary.differentiableOn (λ z hz => hU.bary hz ht) - have φ_derz {z} (hz : z ∈ U) {t} (ht : t ∈ I) : HasDerivAt (λ x => φ x t) (ψ z t) z := by - convert (f_deri (hU.bary hz ht)).comp z hasDerivAt_bary' ; simp [ψ] ; ring - have φ_dert {t} (ht : t ∈ I) : HasDerivAt (φ z) ((z - z₀) * _root_.deriv f ((1 - t) • z₀ + t • z)) t := by - convert (f_deri (hU.bary hz ht)).comp t has_deriv_at_bary using 1 ; ring - have ψ_cont : ContinuousOn (ψ z) I := - continuousOn_id.smul (f_cder.comp continuous_bary.continuousOn (hU.bary hz)) - - have step1 : HasDerivAt (λ z => ∫ t in (0:ℝ)..1, φ z t) (∫ t in (0:ℝ)..1, ψ z t) z := by - obtain ⟨δ, δ_pos, K_subs⟩ := - isCompact_segment.exists_cthickening_subset_open hU' (hU.segment_subset hz) - let K := cthickening δ (segment ℝ z₀ z) - have hz₀ : z₀ ∈ K := self_subset_cthickening _ ⟨1, 0, zero_le_one, le_rfl, by ring, by simp⟩ - have K_cpct : IsCompact K := isCompact_of_isClosed_isBounded isClosed_cthickening - isCompact_segment.isBounded.cthickening - have K_conv : Convex ℝ K := (convex_segment _ _).cthickening _ - have K_ball : ball z δ ⊆ K := ball_subset_closedBall.trans - (closedBall_subset_cthickening (right_mem_segment _ _ _) δ) - obtain ⟨C, hC⟩ := K_cpct.exists_bound_of_continuousOn (f_cder.mono K_subs) - have C_nonneg : 0 ≤ C := (norm_nonneg _).trans (hC z₀ hz₀) - - have key : ∀ t ∈ I, LipschitzOnWith (Real.nnabs C) (φ · t) K := by - refine λ t ht => lipschitzOnWith_iff_norm_sub_le.mpr (λ x hx y hy => ?_) - refine K_conv.norm_image_sub_le_of_norm_deriv_le (f := (φ · t)) (λ w hw => ?_) ?_ hy hx - · exact (φ_diff ht).differentiableAt (hU'.mem_nhds (K_subs hw)) - · rintro w hw - rw [(φ_derz (K_subs hw) ht).deriv] - have f_bary := hC _ ((K_conv.starConvex hz₀).bary hw ht) - have ht' : |t| ≤ 1 := by { rw [abs_le] ; constructor <;> linarith [ht.1, ht.2] } - simpa [ψ, abs_eq_self.2 C_nonneg] using mul_le_mul ht' f_bary (by simp) (by simp) - - apply has_deriv_at_integral_of_continuous_of_lip zero_le_one δ_pos - · exact eventually_of_mem (hU'.mem_nhds hz) (λ _ => φ_cont) - · exact λ t ht => φ_derz hz (Ioc_subset_Icc_self ht) - · exact λ t ht => (key t (Ioc_subset_Icc_self ht)).mono K_ball - · exact ψ_cont.mono Ioc_subset_Icc_self - - have step2 : (∫ t in (0:ℝ)..1, φ z t) + (z - z₀) * (∫ t in (0:ℝ)..1, ψ z t) = f z := by - let g (t : ℝ) : ℂ := t • φ z t - let h (t : ℝ) : ℂ := φ z t + (z - z₀) * ψ z t - - have g_cont : ContinuousOn g I := continuousOn_id.smul (φ_cont hz) - have g_dert : ∀ t ∈ Ioo (0:ℝ) 1, HasDerivAt g (h t) t := by - rintro t ht - convert (hasDerivAt_id t).smul (φ_dert (Ioo_subset_Icc_self ht)) using 1 - simp [ψ, h, add_comm] ; ring - have h_intg : IntervalIntegrable h volume (0:ℝ) 1 := by - apply ContinuousOn.intervalIntegrable - simp only [h, Interval, min_eq_left, zero_le_one, max_eq_right] - convert (φ_cont hz).add (continuousOn_const.mul ψ_cont) ; simp - - convert ← integral_eq_sub_of_hasDerivAt_of_le zero_le_one g_cont g_dert h_intg using 1 - · simp only [ψ, h] - rw [intervalIntegral.integral_add] - · simp - · apply ContinuousOn.intervalIntegrable ; convert φ_cont hz ; simp [Interval] - · apply ContinuousOn.intervalIntegrable - refine continuousOn_const.mul ?_ - convert ψ_cont - simp - · simp [g, φ, detail.φ] - - have : HasDerivAt (primitive f z₀) - ((∫ t in (0:ℝ)..1, φ z t) + (z - z₀) * ∫ t in (0:ℝ)..1, ψ z t) z := by - convert ((hasDerivAt_id z).sub (hasDerivAt_const z z₀)).mul step1 using 1 - simp - - exact step2 ▸ this diff --git a/RMT4/RV.lean b/RMT4/RV.lean deleted file mode 100644 index 70fe7e3..0000000 --- a/RMT4/RV.lean +++ /dev/null @@ -1,31 +0,0 @@ -import Mathlib.Tactic - -open Prod Function - -variable {Ω Ω' α α₁ α₂ : Type*} - -@[ext] structure RV (Ω : Type*) := (toFun : Ω → ℝ) - -instance : CoeFun (RV Ω) (fun _ => Ω → ℝ) := ⟨RV.toFun⟩ -instance : Add (RV Ω) := ⟨(⟨· + ·⟩)⟩ - -class compatible (α₁ α₂ : Type*) := - (α : Type*) - (proj₁ : α → α₁) - (proj₂ : α → α₂) - -instance : compatible Ω Ω := ⟨Ω, id, id⟩ -instance : compatible Ω (Ω × Ω') := ⟨Ω × Ω', fst, id⟩ -instance : compatible (Ω × Ω') Ω := ⟨Ω × Ω', id, fst⟩ - -instance [T : compatible α₁ α₂] : Coe (RV α₁) (RV T.α) := ⟨λ X => ⟨X ∘ T.proj₁⟩⟩ -instance [T : compatible α₁ α₂] : Coe (RV α₂) (RV T.α) := ⟨λ X => ⟨X ∘ T.proj₂⟩⟩ - -instance [T : compatible α₁ α₂] : HAdd (RV α₁) (RV α₂) (RV T.α) := ⟨(· + ·)⟩ - -def copy (X : RV Ω) : RV (Ω × Ω) := ⟨X ∘ snd⟩ - -def double₁ (X : RV Ω) := X + copy X -def double₂ (X : RV Ω) := copy X + X - -example (X : RV Ω) : double₁ X = double₂ X := by ext ω ; apply add_comm diff --git a/RMT4/Subdivision.lean b/RMT4/Subdivision.lean deleted file mode 100644 index 2d43180..0000000 --- a/RMT4/Subdivision.lean +++ /dev/null @@ -1,333 +0,0 @@ -import Mathlib.Tactic -import RMT4.to_mathlib - -open Set Function List Topology BigOperators Nat Filter - -abbrev Subdivision (a b : ℝ) := Finset (Ioo a b) - -namespace Subdivision - -variable {a b a' b' t c d : ℝ} {σ : Subdivision a b} - -section basic - -def cast (σ : Subdivision a b) (ha : a = a') (hb : b = b') : Subdivision a' b' := ha ▸ hb ▸ σ - -def size (σ : Subdivision a b) : ℕ := Finset.card σ - -noncomputable def toList (σ : Subdivision a b) : List ℝ := - a :: (Finset.sort (· ≤ ·) σ).map Subtype.val ++ [b] - -@[simp] lemma toList_length : σ.toList.length = σ.size + 2 := by simp [toList, size] - -lemma toList_sorted (hab : a < b) : σ.toList.Sorted (· < ·) := by - simp only [toList, cons_append, sorted_cons, mem_append, Finset.mem_sort, List.mem_singleton] - constructor - · intro t ht ; cases ht with - | inl h => obtain ⟨u₁, _, rfl⟩ := List.mem_map.1 h ; exact u₁.prop.1 - | inr h => linarith - . simp [Sorted, pairwise_append] ; constructor - · apply (Finset.sort_sorted_lt _).map ; exact fun _ _ => id - · rintro t ⟨_, h₂⟩ _ ; exact h₂ - -noncomputable def toFun (σ : Subdivision a b) : Fin (σ.size + 2) → ℝ := - σ.toList.get ∘ Fin.cast toList_length.symm - -noncomputable instance : CoeFun (Subdivision a b) (λ σ => Fin (σ.size + 2) → ℝ) := ⟨toFun⟩ - -lemma mem_iff (σ : Subdivision a b) : t ∈ σ.toList ↔ ∃ i, σ i = t := by - rw [mem_iff_get] - constructor <;> rintro ⟨i, hi⟩ <;> exact ⟨Fin.cast (by simp) i, hi⟩ - -noncomputable abbrev x (σ : Subdivision a b) (i : Fin (σ.size + 1)) : ℝ := σ i.castSucc - -noncomputable abbrev y (σ : Subdivision a b) (i : Fin (σ.size + 1)) : ℝ := σ i.succ - -lemma mono (hab : a < b) : StrictMono σ.toFun := - (toList_sorted hab).get_strictMono.comp (λ _ _ => id) - -lemma mono' (hab : a < b) {i : Fin (σ.size + 1)} : σ.x i < σ.y i := - Fin.strictMono_iff_lt_succ.1 (σ.mono hab) i - -@[simp] lemma first : σ 0 = a := rfl - -@[simp] lemma last : σ (Fin.last _) = b := by convert List.get_last _ ; simp - -lemma toList_subset (hab : a ≤ b) (ht : t ∈ σ.toList) : t ∈ Icc a b := by - simp [toList] at ht - rcases ht with rfl | ⟨h, _⟩ | rfl - · exact left_mem_Icc.2 hab - · exact ⟨h.1.le, h.2.le⟩ - · exact right_mem_Icc.2 hab - -lemma subset {i : Fin (σ.size + 2)} (hab : a ≤ b) : σ i ∈ Icc a b := - toList_subset hab (by simpa [toFun] using List.get_mem _ _ _) - -end basic - -section pieces - -def piece (σ : Subdivision a b) (i : Fin (σ.size + 1)) : Set ℝ := Icc (σ.x i) (σ.y i) - -lemma piece_subset {i : Fin (σ.size + 1)} (hab : a ≤ b) : σ.piece i ⊆ Icc a b := - Icc_subset_Icc (subset hab).1 (subset hab).2 - -noncomputable def length (σ : Subdivision a b) (i : Fin (σ.size + 1)) : ℝ := σ.y i - σ.x i - -noncomputable def lengths (σ : Subdivision a b) : Finset ℝ := Finset.univ.image σ.length - -noncomputable def mesh (σ : Subdivision a b) : ℝ := σ.lengths.max' (Finset.univ_nonempty.image _) - -lemma le_mesh {i : Fin (σ.size + 1)} : σ.y i - σ.x i ≤ σ.mesh := by - apply Finset.le_max' _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ i)) - -@[simp] lemma union0 {α : Type*} {s : Fin 1 → Set α} : ⋃ i : Fin 1, s i = s 0 := ciSup_unique - -lemma cover1 (n : ℕ) (f : Fin (n + 2) → ℝ) (hf : Monotone f) : - ⋃ i : Fin (n + 1), Icc (f i.castSucc) (f i.succ) ⊆ Icc (f 0) (f (Fin.last (n + 1))) := by - apply iUnion_subset - rintro i t ⟨h1, h2⟩ - constructor <;> linarith [hf (Fin.zero_le (Fin.castSucc i)), hf (Fin.le_last (Fin.succ i))] - -lemma cover2 (n : ℕ) (f : Fin (n + 2) → ℝ) : Icc (f 0) (f (Fin.last (n + 1))) ⊆ - ⋃ i : Fin (n + 1), Icc (f i.castSucc) (f i.succ) := by - induction n with - | zero => rw [union0] ; rfl - | succ n ih => - intro t ht - cases Icc_subset_Icc_union_Icc (b := f (Fin.last n.succ).castSucc) ht with - | inl h => - obtain ⟨i, hi⟩ := mem_iUnion.1 (ih (f ∘ Fin.castSucc) h) - exact mem_iUnion.2 ⟨_, hi⟩ - | inr h => exact mem_iUnion.2 ⟨_, h⟩ - -lemma cover_aux (n : ℕ) (f : Fin (n + 2) → ℝ) (hf : Monotone f) : - ⋃ i : Fin (n + 1), Icc (f i.castSucc) (f i.succ) = Icc (f 0) (f (Fin.last (n + 1))) := - subset_antisymm (cover1 n f hf) (cover2 n f) - -lemma cover (σ : Subdivision a b) (hab : a < b) : ⋃ i : _, σ.piece i = Icc a b := by - simp only [piece, x, y] - convert cover_aux _ _ (mono hab).monotone - simp - -lemma cover' (hab : a < b) (t : Icc a b) : ∃ i, ↑t ∈ σ.piece i := by - rcases t with ⟨t, ht⟩ - rw [← σ.cover hab, mem_iUnion] at ht - exact ht - -end pieces - -section order - -variable {τ : Subdivision a b} - -lemma aux (h : σ ≤ τ) : map Subtype.val (Finset.sort (· ≤ ·) σ) ⊆ - map Subtype.val (Finset.sort (· ≤ ·) τ) := by - refine map_subset _ (λ t ht => ?_) - rw [Finset.mem_sort] at ht ⊢ - exact h ht - -lemma toList_le_of_le (h : σ ≤ τ) : σ.toList ⊆ τ.toList := by - simpa [toList] using (aux h).trans (subset_cons_of_subset _ (subset_append_left _ _)) - -lemma piece_subset_of_le (hab : a < b) (hστ : σ ≤ τ) (j) : ∃ i, τ.piece j ⊆ σ.piece i := by - let t := (1/2) * τ.x j + (1/2) * τ.y j - have l1 : t ∈ Ioo (τ.x j) (τ.y j) := (Convex.mem_Ioo (mono' hab)).2 ⟨1/2, 1/2, by norm_num⟩ - obtain ⟨i, hi⟩ := cover' hab ⟨t, τ.piece_subset hab.le (Ioo_subset_Icc_self l1)⟩ - refine ⟨i, Icc_subset_Icc ?_ ?_⟩ - · have : σ.x i ∈ σ.toList := σ.mem_iff.2 ⟨_, rfl⟩ - obtain ⟨k, l11⟩ := τ.mem_iff.1 (toList_le_of_le hστ this) - refine l11 ▸ (mono hab).monotone ?_ - rw [Fin.le_castSucc_iff, (mono hab).lt_iff_lt.symm, l11] - exact hi.1.trans_lt l1.2 - · have l12 : σ.y i ∈ σ.toList := σ.mem_iff.2 ⟨i.succ, rfl⟩ - obtain ⟨l, l14⟩ := τ.mem_iff.1 (toList_le_of_le hστ l12) - refine l14 ▸ (mono hab).monotone ?_ - rw [← Fin.castSucc_lt_iff_succ_le, (mono hab).lt_iff_lt.symm, l14] - exact l1.1.trans_le hi.2 - -lemma sub_le_sub_of_Icc (hab : a ≤ b) (h : Icc a b ⊆ Icc c d) : b - a ≤ d - c := by - linarith [(Icc_subset_Icc_iff hab).1 h] - -lemma mesh_antitone (hab : a < b) : Antitone (mesh : Subdivision a b → ℝ) := by - intro σ τ hστ - apply Finset.max'_le - intro ℓ hℓ - obtain ⟨i, _, rfl⟩ := Finset.mem_image.1 hℓ - obtain ⟨j, hj⟩ := piece_subset_of_le hab hστ i - exact (sub_le_sub_of_Icc (mono' hab).le hj).trans le_mesh - -end order - -namespace regular - -variable {n i : ℕ} - -noncomputable def aux (a b : ℝ) (n i : ℕ) : ℝ := a + i * ((b - a) / (n + 1)) - -@[simp] lemma aux_zero : aux a b n 0 = a := by simp [aux] - -@[simp] lemma aux_last : aux a b n (n + 1) = b := by field_simp [aux] ; ring - -lemma aux_mono (hab : a < b) : StrictMono (aux a b n) := by - have := sub_pos.2 hab - intro i j hij - simp only [aux, add_lt_add_iff_left] - gcongr ; simp [hij] - -lemma aux_mem_Ioo (hab : a < b) (h : i < n) : aux a b n (i + 1) ∈ Ioo a b := by - constructor - · convert aux_mono hab (succ_pos i) ; simp - · convert aux_mono hab (succ_lt_succ h) ; simp - -noncomputable def list (a b : ℝ) (n : ℕ) : List ℝ := - (List.range n).map (λ i => aux a b n (i + 1)) - -lemma list_sorted (hab : a < b) : (list a b n).Sorted (· < ·) := - (pairwise_lt_range n).map _ (λ _ _ hij => aux_mono hab (succ_lt_succ hij)) - -lemma list_mem_Ioo (hab : a < b) : ∀ x ∈ list a b n, x ∈ Ioo a b := by - simp only [list, List.mem_map, List.mem_range, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] - exact λ i hi => aux_mem_Ioo hab hi - -noncomputable def list' (hab : a < b) (n : ℕ) : List (Ioo a b) := - (list a b n).pmap Subtype.mk (list_mem_Ioo hab) - -lemma list'_sorted (hab : a < b) : (list' hab n).Sorted (· < ·) := - (list_sorted hab).pmap _ (λ _ _ _ _ => id) - -noncomputable def _root_.Subdivision.regular (hab : a < b) (n : ℕ) : Subdivision a b := - (list' hab n).toFinset - -@[simp] lemma size (hab : a < b) : (regular hab n).size = n := by - simp [regular, Subdivision.size, toFinset_card_of_nodup, (list'_sorted hab).nodup] - simp [list', list] - -@[simp] lemma eq_aux (hab : a < b) {i : Fin _} : - List.get (a :: (map Subtype.val (list' hab n) ++ [b])) i = aux a b n i := by - apply Fin.cases (motive := λ i => _ = _) (by simp) - intro i - simp only [List.get, add_eq, add_zero, Fin.eta, length_cons, Fin.val_succ] - by_cases h : i < (map Subtype.val (list' hab n)).length - · rcases i with ⟨i, hi⟩ - simp only [List.get_append i h, get_map] - simp [list', List.get_pmap, list] - · simp only [List.get_last h] - convert aux_last.symm - rcases i with ⟨i, h'i⟩ - simp [list', list] at h h'i - linarith - -@[simp] lemma eq (hab : a < b) {i} : regular hab n i = aux a b n i := by - rcases i with ⟨i, hi⟩ - have l1 : Finset.sort (· ≤ ·) (List.toFinset (list' hab n)) = list' hab n := by - apply List.Sorted.toFinset_sort - exact list'_sorted hab - have l3 : i < (a :: (map Subtype.val (list' hab n) ++ [b])).length := by - simpa [list', list] using hi - have l2 : List.get (a :: (map Subtype.val (list' hab n) ++ [b])) ⟨_, l3⟩ = aux a b n i := by - exact eq_aux hab - simp only [toFun, regular, toList, cons_append, length_cons, comp_apply] - convert l2 - simp [toFinset_card_of_nodup, (list'_sorted hab).nodup] - -@[simp] lemma length_eq (hab : a < b) {i : Fin _} : - length (regular hab n) i = (b - a) / (n + 1) := by - have (i x : ℝ) : (i + 1) * x - i * x = x := by ring - simp [length, aux, this, x, y] - -@[simp] lemma lengths_eq (hab : a < b) : lengths (regular hab n) = { (b - a) / (n + 1) } := by - have : length (regular hab n) = λ (i : Fin _) => (b - a) / (n + 1) := by ext; simp - rw [lengths, this] - apply Finset.image_const Finset.univ_nonempty - -@[simp] lemma mesh_eq (hab : a < b) : (regular hab n).mesh = (b - a) / (n + 1) := by - simp [mesh, hab] - -end regular - -section adapted - -variable {ι : Type*} {S : ι → Set ℝ} - -structure Adaptation (σ : Subdivision a b) (S : ι → Set ℝ) := - I : Fin (σ.size + 1) → ι - hI k : σ.piece k ⊆ S (I k) - -def IsAdapted (σ : Subdivision a b) (S : ι → Set ℝ) : Prop := Nonempty (Adaptation σ S) - -lemma isAdapted_of_mesh_lt (hab : a < b) (h1 : ∀ i, IsOpen (S i)) (h2 : Icc a b ⊆ ⋃ i, S i) : - ∃ ε > 0, ∀ σ : Subdivision a b, σ.mesh < ε → IsAdapted σ S := by - obtain ⟨ε, hε, l1⟩ := lebesgue_number_lemma_of_metric isCompact_Icc h1 h2 - refine ⟨ε, hε, λ σ hσ => ?_⟩ - choose I hI using l1 - refine ⟨λ j => I (σ.x j) (σ.subset hab.le), λ j => ?_⟩ - have : Set.OrdConnected (Metric.ball (σ.x j) ε) := (convex_ball ..).ordConnected - refine subset_trans ?_ (hI (σ.x j) (σ.subset hab.le)) - refine Set.Icc_subset _ (Metric.mem_ball_self hε) ?_ - simp only [Metric.mem_ball] - convert (le_mesh (i := j)).trans_lt hσ using 1 - refine abs_eq_self.2 (sub_nonneg.2 (σ.mono hab Fin.lt_succ).le) - -lemma isAdapted_of_mesh_le (hab : a < b) (h1 : ∀ i, IsOpen (S i)) (h2 : Icc a b ⊆ ⋃ i, S i) : - ∃ ε > 0, ∀ σ : Subdivision a b, σ.mesh ≤ ε → IsAdapted σ S := by - obtain ⟨ε, hε, h⟩ := isAdapted_of_mesh_lt hab h1 h2 - refine ⟨ε / 2, by positivity, λ σ hσ => h σ (by linarith)⟩ - -structure AdaptedSubdivision (a b : ℝ) (S : ι → Set ℝ) := - σ : Subdivision a b - h : Adaptation σ S - -noncomputable def exists_adapted (hab : a < b) (h1 : ∀ i, IsOpen (S i)) (h2 : Icc a b ⊆ ⋃ i, S i) : - Nonempty (AdaptedSubdivision a b S) := by - choose ε hε h using isAdapted_of_mesh_le hab h1 h2 - choose n hn using exists_div_lt (b - a) hε - have : (regular hab n).mesh = (b - a) / ↑(n + 1) := by simp - exact ⟨_, (h (regular hab n) (by linarith)).some⟩ - -noncomputable def exists_adapted' (hab : a < b) (h : ∀ t : Icc a b, ∃ i, S i ∈ 𝓝[Icc a b] t.1) : - Nonempty (AdaptedSubdivision a b S) := by - choose I hI using h - choose S' h1 h2 using λ t => (nhdsWithin_basis_open t.1 (Icc a b)).mem_iff.1 (hI t) - have : Icc a b ⊆ ⋃ t, S' t := λ t ht => mem_iUnion.2 ⟨⟨t, ht⟩, (h1 ⟨t, ht⟩).1⟩ - obtain ⟨σ, hσ1, hσ2⟩ := exists_adapted hab (λ t => (h1 t).2) this - exact ⟨σ, I ∘ hσ1, λ k => (Set.subset_inter (hσ2 k) (σ.piece_subset hab.le)).trans (h2 (hσ1 k))⟩ - -structure RelAdaptedSubdivision (a b : ℝ) (S : ι → Set ℂ) (γ : ℝ → ℂ) := - σ : Subdivision a b - I : Fin (σ.size + 1) → ι - sub k : γ '' σ.piece k ⊆ S (I k) - -noncomputable def exists_reladapted {γ : ℝ → ℂ} {S : ι → Set ℂ} (hab : a < b) - (hγ : ContinuousOn γ (Icc a b)) (h : ∀ t : Icc a b, ∃ i, S i ∈ 𝓝 (γ t.1)) : - Nonempty (RelAdaptedSubdivision a b S γ) := by - choose I hI using h - obtain ⟨σ, K, hK⟩ := exists_adapted' hab (λ t => ⟨t, hγ _ t.2 (hI t)⟩) - exact ⟨σ, I ∘ K, λ k => image_subset_iff.2 (hK k)⟩ - -end adapted - -section sum - -noncomputable def sum (σ : Subdivision a b) (f : Fin (σ.size + 1) → ℝ → ℝ → ℂ) : ℂ := - ∑ i : _, f i (σ.x i) (σ.y i) - -noncomputable abbrev sumSub (σ : Subdivision a b) (F : Fin (σ.size + 1) → ℝ → ℂ) : ℂ := - σ.sum (λ i x y => F i y - F i x) - -noncomputable abbrev sumSubAlong (σ : Subdivision a b) (F : Fin (σ.size + 1) → ℂ → ℂ) - (γ : ℝ → ℂ) : ℂ := - sumSub σ (λ i => F i ∘ γ) - -variable {F G : Fin (σ.size + 1) → ℝ → ℝ → ℂ} - -lemma sum_eq_zero (h : ∀ i, F i (σ.x i) (σ.y i) = 0) : σ.sum F = 0 := - Finset.sum_eq_zero (λ i _ => h i) - -lemma sum_congr (h : ∀ i, F i (σ.x i) (σ.y i) = G i (σ.x i) (σ.y i)) : - σ.sum F = σ.sum G := - Finset.sum_congr rfl (λ i _ => h i) - -end sum - -end Subdivision diff --git a/RMT4/cindex.lean b/RMT4/cindex.lean index 8e15214..ce191d3 100644 --- a/RMT4/cindex.lean +++ b/RMT4/cindex.lean @@ -2,8 +2,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros import Mathlib.Analysis.Complex.RemovableSingularity import Mathlib.MeasureTheory.Integral.CircleIntegral -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) - open Real Complex Function TopologicalSpace Filter Topology Metric MeasureTheory Nat noncomputable def cindex (z₀ : ℂ) (r : ℝ) (f : ℂ → ℂ) : ℂ := diff --git a/RMT4/etape2.lean b/RMT4/etape2.lean index 241b1d6..da3d1d9 100644 --- a/RMT4/etape2.lean +++ b/RMT4/etape2.lean @@ -2,8 +2,6 @@ import Mathlib.Analysis.Complex.Schwarz import RMT4.defs import RMT4.to_mathlib -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) - open Complex ComplexConjugate Set Metric Topology Filter namespace RMT diff --git a/RMT4/pintegral.lean b/RMT4/pintegral.lean deleted file mode 100644 index 29f1e6d..0000000 --- a/RMT4/pintegral.lean +++ /dev/null @@ -1,206 +0,0 @@ -import RMT4.LocallyConstant -import RMT4.Primitive -import RMT4.Subdivision - -open BigOperators Metric Set Subdivision Topology Filter Nat - -variable {s t U V : Set ℂ} {z z₀ : ℂ} {f F : ℂ → ℂ} {a b : ℝ} {γ : ℝ → ℂ} {n : ℕ} - -structure LocalPrimitiveOn (s : Set ℂ) (f : ℂ → ℂ) := - F : s → ℂ → ℂ - S : s → Set ℂ - mem (z : s) : z.1 ∈ S z - opn (z : s) : IsOpen (S z) - der (z : s) : ∀ w ∈ S z, HasDerivAt (F z) (f w) w - -namespace LocalPrimitiveOn - -lemma nhd (h : LocalPrimitiveOn s f) (z : s) : h.S z ∈ 𝓝 z.1 := - (h.opn z).mem_nhds (h.mem z) - -def restrict (Λ : LocalPrimitiveOn s f) (h : t ⊆ s) : LocalPrimitiveOn t f where - F := Λ.F ∘ inclusion h - S := Λ.S ∘ inclusion h - mem z := Λ.mem (inclusion h z) - opn z := Λ.opn (inclusion h z) - der z := Λ.der (inclusion h z) - -def zero : LocalPrimitiveOn univ 0 where - F _ := 0 - S _ := univ - mem _ := mem_univ _ - opn _ := isOpen_univ - der _ _ _ := hasDerivAt_const _ _ - -protected noncomputable def deriv {{U : Set ℂ}} (hU : IsOpen U) {{F : ℂ → ℂ}} - (hF : DifferentiableOn ℂ F U) : LocalPrimitiveOn U (deriv F) where - F _ := F - S _ := U - mem z := z.2 - opn _ := hU - der _ _ hw := DifferentiableAt.hasDerivAt (hF.differentiableAt (hU.mem_nhds hw)) - -noncomputable def inradius {U : Set ℂ} (hU : IsOpen U) (hz : z ∈ U) : - {ε // 0 < ε ∧ ball z ε ⊆ U} := by - choose ε ε_pos hε using isOpen_iff.1 hU z hz - exact ⟨ε, ε_pos, hε⟩ - -lemma hasDerivAt_inradius {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hz₀ : z₀ ∈ U) - (hz : z ∈ ball z₀ (inradius hU hz₀)) : HasDerivAt (primitive f z₀) (f z) z := by - have l1 : StarConvex ℝ z₀ (ball z₀ (inradius hU hz₀)) := - (convex_ball _ _).starConvex (mem_ball_self (inradius hU hz₀).2.1) - exact (hf.mono (inradius hU hz₀).2.2).exists_primitive l1 isOpen_ball hz - -noncomputable def of_differentiableOn {U : Set ℂ} (hU : IsOpen U) {f : ℂ → ℂ} - (h : DifferentiableOn ℂ f U) : LocalPrimitiveOn U f where - F z := primitive f z - S z := ball z (inradius hU z.2) - mem z := mem_ball_self (inradius hU z.2).2.1 - opn _ := isOpen_ball - der z _ hw := hasDerivAt_inradius hU h z.2 hw - -end LocalPrimitiveOn - -def HasLocalPrimitiveOn (U : Set ℂ) (f : ℂ → ℂ) : Prop := Nonempty (LocalPrimitiveOn U f) - -namespace HasLocalPrimitiveOn - -lemma iff : HasLocalPrimitiveOn U f ↔ ∀ z ∈ U, ∃ F, ∀ᶠ w in 𝓝 z, HasDerivAt F (f w) w where - mp := by - intro ⟨F, S, mem, opn, der⟩ z hz - use F ⟨z, hz⟩ - apply eventually_of_mem ((opn ⟨z, hz⟩).mem_nhds (mem ⟨z, hz⟩)) - intro x hx - exact der ⟨z, hz⟩ x hx - mpr h := by - simp only [eventually_nhds_iff_ball] at h - choose! F ε hε h using h - refine ⟨λ z => F z, λ z => ball z (ε z), ?_, ?_, ?_⟩ - · exact λ z => mem_ball_self $ hε z z.2 - · exact λ z => isOpen_ball - · exact λ z => h z z.2 - -lemma mono (h : HasLocalPrimitiveOn U f) (hVU : V ⊆ U) : HasLocalPrimitiveOn V f := - ⟨h.some.restrict hVU⟩ - -lemma zero : HasLocalPrimitiveOn s 0 := ⟨LocalPrimitiveOn.zero.restrict (subset_univ _)⟩ - -lemma deriv (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) : HasLocalPrimitiveOn U (deriv F) := - ⟨LocalPrimitiveOn.deriv hU hF⟩ - -lemma holo (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) : HasLocalPrimitiveOn U F := - ⟨LocalPrimitiveOn.of_differentiableOn hU hF⟩ - -end HasLocalPrimitiveOn - -section pintegral - -variable {a b : ℝ} {γ : ℝ → ℂ} {f : ℂ → ℂ} - -noncomputable def pintegral_aux (hab : a < b) (hγ : ContinuousOn γ (Icc a b)) - (Λ : LocalPrimitiveOn (γ '' Icc a b) f) : ℂ := by - have h1 (t : Icc a b) : ∃ i : γ '' Icc a b, Λ.S i ∈ 𝓝 (γ t) := ⟨⟨γ t, t, t.2, rfl⟩, Λ.nhd _⟩ - obtain RW := (exists_reladapted hab hγ h1).some - exact RW.σ.sumSubAlong (Λ.F ∘ RW.I) γ - -noncomputable def pintegral (a b : ℝ) (f : ℂ → ℂ) (γ : ℝ → ℂ) : ℂ := by - by_cases h : a < b ∧ ContinuousOn γ (Icc a b) ∧ HasLocalPrimitiveOn (γ '' Icc a b) f - · exact pintegral_aux h.1 h.2.1 h.2.2.some - · exact 0 - -lemma apply_eq_of_path (hab : a ≤ b) {f : ℂ → ℂ} (hf : IsLocallyConstant (U.restrict f)) - {γ : ℝ → ℂ} (hγ : ContinuousOn γ (Icc a b)) (h : MapsTo γ (Icc a b) U) : - f (γ b) = f (γ a) := by - haveI : PreconnectedSpace (Icc a b) := isPreconnected_iff_preconnectedSpace.1 isPreconnected_Icc - have h2 := hf.comp_continuous (hγ.restrict_mapsTo h) - exact @IsLocallyConstant.apply_eq_of_isPreconnected _ _ _ _ (h2) _ isPreconnected_univ - ⟨b, hab, le_rfl⟩ ⟨a, le_rfl, hab⟩ (mem_univ _) (mem_univ _) - -lemma sumSubAlong_eq_zero (hab : a < b) (Λ : LocalPrimitiveOn U 0) - (RW : RelAdaptedSubdivision a b Λ.S γ) (hγ : ContinuousOn γ (Icc a b)) : - RW.σ.sumSubAlong (Λ.F ∘ RW.I) γ = 0 := by - refine Subdivision.sum_eq_zero (λ k => (sub_eq_zero.2 ?_)) - apply apply_eq_of_path (RW.σ.mono' hab).le - · apply isLocallyConstant_of_deriv_eq_zero (Λ.opn (RW.I k)) - · exact λ z hz => (Λ.der (RW.I k) z hz).differentiableAt.differentiableWithinAt - · exact λ z hz => (Λ.der (RW.I k) z hz).deriv - · exact hγ.mono (RW.σ.piece_subset hab.le) - · exact mapsTo'.2 (RW.sub k) - -@[simp] lemma pintegral_zero (hab : a < b) (hγ : ContinuousOn γ (Icc a b)) : - pintegral a b 0 γ = 0 := by - have : HasLocalPrimitiveOn (γ '' Icc a b) 0 := ⟨LocalPrimitiveOn.zero.restrict (subset_univ _)⟩ - simp [pintegral, hab, hγ, this, pintegral_aux, sumSubAlong_eq_zero] - -end pintegral - -lemma sub_eq_sub_of_deriv_eq_deriv (hab : a ≤ b) (hU : IsOpen U) - {γ : ℝ → ℂ} (hγ₁ : ContinuousOn γ (Icc a b)) (hγ₂ : MapsTo γ (Icc a b) U) - {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) - (hfg : ∀ z ∈ U, deriv f z = deriv g z) : - f (γ b) - f (γ a) = g (γ b) - g (γ a) := by - rw [sub_eq_sub_iff_sub_eq_sub] - change (f - g) (γ b) = (f - g) (γ a) - refine apply_eq_of_path hab ?_ hγ₁ hγ₂ - refine isLocallyConstant_of_deriv_eq_zero hU (hf.sub hg) (λ z hz => ?_) - have h1 : DifferentiableAt ℂ f z := hf.differentiableAt (hU.mem_nhds hz) - have h2 : DifferentiableAt ℂ g z := hg.differentiableAt (hU.mem_nhds hz) - have h3 : deriv (f - g) z = deriv f z - deriv g z := deriv_sub h1 h2 - simp [hfg z hz, h3] - -lemma sumSubAlong_eq_of_sigma (hab : a < b) {hf : LocalPrimitiveOn U f} - {RW₁ RW₂ : RelAdaptedSubdivision a b hf.S γ} (h : RW₁.σ = RW₂.σ) - (hγ : ContinuousOn γ (Icc a b)) : - RW₁.σ.sumSubAlong (hf.F ∘ RW₁.I) γ = RW₂.σ.sumSubAlong (hf.F ∘ RW₂.I) γ := by - rcases hf with ⟨F, S, _, Sopn, Sder⟩ - rcases RW₁ with ⟨σ, I₁, hI₁⟩ - rcases RW₂ with ⟨σ', I₂, hI₂⟩ - subst h - refine Subdivision.sum_congr (λ k => ?_) - apply sub_eq_sub_of_deriv_eq_deriv (σ.mono' hab).le ((Sopn _).inter (Sopn _)) - · exact (hγ.mono (σ.piece_subset hab.le)) - · simpa only [mapsTo'] using subset_inter (hI₁ k) (hI₂ k) - · exact λ z hz => (Sder (I₁ k) z hz.1).differentiableAt.differentiableWithinAt - · exact λ z hz => (Sder (I₂ k) z hz.2).differentiableAt.differentiableWithinAt - · intro z hz - have l1 := (Sder (I₁ k) z hz.1).deriv - have l2 := (Sder (I₂ k) z hz.2).deriv - simp only at l1 l2 - simp only [Function.comp_apply, l1, l2] - -lemma telescopic (f : Fin (n + 1) → ℂ) : - ∑ i : Fin n, (f i.succ - f i.castSucc) = f (Fin.last n) - f 0 := by - have l1 : ∑ i : Fin n, f (i.succ) = ∑ i : Fin (n + 1), f i - f 0 := by - simp [Fin.sum_univ_succ f] - have l2 : ∑ i : Fin n, f (i.castSucc) = ∑ i : Fin (n + 1), f i - f (Fin.last n) := by - simp [Fin.sum_univ_castSucc f] - simp [l1, l2] - -lemma sumSubAlong_eq_sub - (hab : a < b) - (hF : DifferentiableOn ℂ F U) - (hf : LocalPrimitiveOn (γ '' Icc a b) (deriv F)) - (hγ : ContinuousOn γ (Icc a b)) - (RW : RelAdaptedSubdivision a b hf.S γ) - (hU : IsOpen U) - (hh : MapsTo γ (Icc a b) U) : - RW.σ.sumSubAlong (hf.F ∘ RW.I) γ = F (γ b) - F (γ a) := by - have key (i) : ((hf.F ∘ RW.I) i ∘ γ) (RW.σ.y i) - ((hf.F ∘ RW.I) i ∘ γ) (RW.σ.x i) = - F (γ (RW.σ.y i)) - F (γ (RW.σ.x i)) := by - apply sub_eq_sub_of_deriv_eq_deriv - · exact (RW.σ.mono' hab).le - · exact (hf.opn (RW.I i)).inter hU - · exact hγ.mono (RW.σ.piece_subset hab.le) - · exact (Set.mapsTo'.2 (RW.sub i)).inter (hh.mono_left (RW.σ.piece_subset hab.le)) - · exact λ z hz => by exact (hf.der (RW.I i) z hz.1).differentiableAt.differentiableWithinAt - · exact DifferentiableOn.mono hF (inter_subset_right _ _) - · exact λ z hz => (hf.der (RW.I i) z hz.1).deriv - simp only [sumSubAlong, sumSub, sum, key] - convert telescopic (F ∘ γ ∘ RW.σ) - simp only [← RW.σ.last] ; rfl - -lemma pintegral_deriv {F : ℂ → ℂ} {γ : ℝ → ℂ} (hab : a < b) (hU : IsOpen U) - (hγ : ContinuousOn γ (Icc a b)) (h2 : MapsTo γ (Icc a b) U) (hF : DifferentiableOn ℂ F U) : - pintegral a b (deriv F) γ = F (γ b) - F (γ a) := by - simpa [pintegral, hab, hγ, (HasLocalPrimitiveOn.deriv hU hF).mono (mapsTo'.1 h2)] - using sumSubAlong_eq_sub hab hF _ hγ _ hU h2