Refactor

RMT4.lean

@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Complex.OpenMapping
-import RMT4.Basic
 import RMT4.cindex
 import RMT4.defs
 import RMT4.deriv_inj
@@ -8,5 +7,6 @@ import RMT4.has_sqrt
 import RMT4.hurwitz
 import RMT4.Main
 import RMT4.Montel
+import RMT4.Spaces
 import RMT4.to_mathlib
 import RMT4.uniform

RMT4/Main.lean

@@ -1,4 +1,4 @@
-import RMT4.Basic
+import RMT4.Spaces
 import RMT4.etape2
 import RMT4.has_sqrt
 import RMT4.Montel
@@ -7,75 +7,6 @@ open UniformConvergence Topology Filter Set Metric Function
 
 variable {ι : Type*} {l : Filter ι} {U : Set ℂ} {z₀ : ℂ}
 
-namespace RMT
-
--- `𝓜 U` : holomorphic functions to the unit closed ball
-
-def 𝓜 (U : Set ℂ) := {f ∈ 𝓗 U | MapsTo f U (closedBall (0 : ℂ) 1)}
-
-example : 𝓜 U = 𝓑 U (fun _ => closedBall 0 1) := 𝓑_const.symm
-
-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)} 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)
-    (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous)
-
--- `𝓘 U` : holomorphic injections into the unit ball
-
-def 𝓘 (U : Set ℂ) := {f ∈ 𝓜 U | InjOn f U}
-
-lemma 𝓘_nonempty [good_domain U] : (𝓘 U).Nonempty := by
-  obtain ⟨u, hu⟩ := nonempty_compl.mpr (good_domain.ne_univ : U ≠ univ)
-  let f : ℂ → ℂ := λ z => z - u
-  have f_inj : Injective f := λ _ _ h => sub_left_inj.mp h
-  have f_hol : DifferentiableOn ℂ f U := differentiableOn_id.sub (differentiableOn_const u)
-  have f_noz : ∀ ⦃z : ℂ⦄, z ∈ U -> f z ≠ 0 := λ z hz f0 => hu (sub_eq_zero.mp f0 ▸ hz)
-
-  obtain ⟨g, g_hol, g_sqf⟩ := good_domain.has_sqrt f f_noz f_hol
-  obtain ⟨z₀, hz₀⟩ := (good_domain.is_nonempty : U.Nonempty)
-
-  have gU_nhd : g '' U ∈ 𝓝 (g z₀) := by
-    have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
-    have e2 := g_hol.analyticAt e1
-    have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
-    have dg_nonzero : deriv g z₀ ≠ 0 := by
-      have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
-      simp [e3, deriv_sub_const, f]
-      intro h
-      have := g_sqf hz₀
-      rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
-      cases f_noz hz₀ this
-    refine e2.eventually_constant_or_nhds_le_map_nhds.resolve_left (λ h => ?_) (image_mem_map e1)
-    simp [EventuallyEq.deriv_eq h] at dg_nonzero
-
-  obtain ⟨r, r_pos, hr⟩ := Metric.mem_nhds_iff.mp gU_nhd
-  let gg : RMT.embedding U ((closedBall (- g z₀) (r / 2))ᶜ) :=
-  { to_fun := g,
-    is_diff := g_hol,
-    is_inj := λ z₁ hz₁ z₂ hz₂ hgz => f_inj (by simp [g_sqf _, hz₁, hz₂, hgz]),
-    maps_to := λ z hz hgz => by {
-      apply f_noz hz
-      rw [mem_closed_ball_neg_iff_mem_neg_closed_ball] at hgz
-      obtain ⟨z', hz', hgz'⟩ := (closedBall_subset_ball (by linarith)).trans hr hgz
-      have hzz' : z = z' := f_inj (by simp [g_sqf hz, g_sqf hz', hgz'])
-      simpa [hzz', neg_eq_self_iff, g_sqf hz'] using hgz'.symm } }
-
-  let ggg := (embedding.inv _ (by linarith)).comp gg
-  refine ⟨ggg.to_fun, ⟨ggg.is_diff, ?_⟩, ggg.is_inj⟩
-  exact λ z hz => ball_subset_closedBall (ggg.maps_to hz)
-
--- `𝓙 U` : the closure of `𝓘 U`, injections and constants
-
-def 𝓙 (U : Set ℂ) := {f ∈ 𝓜 U | InjOn f U ∨ ∃ w : ℂ, EqOn f (λ _ => w) U}
-
-lemma 𝓘_subset_𝓙 : 𝓘 U ⊆ 𝓙 U := λ _ hf => ⟨hf.1, Or.inl hf.2⟩
-
 lemma IsCompact_𝓙 [good_domain U] : IsCompact (𝓙 U) := by
   have hU : IsOpen U := good_domain.is_open
   refine (isCompact_𝓜 hU).of_isClosed_subset ?_ (λ _ hf => hf.1)
@@ -87,7 +18,7 @@ lemma IsCompact_𝓙 [good_domain U] : IsCompact (𝓙 U) := by
   refine ⟨(IsClosed_𝓜 hU).mem_of_tendsto h1 (h2.mono (λ _ h => h.1)), ?_⟩
   by_cases h : ∃ᶠ f in l, InjOn f U
   case pos =>
-    refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_iff hU).1 h1) h).symm
+    refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_𝓒_iff hU).1 h1) h).symm
     filter_upwards [h2] with g hg using hg.1.1
   case neg =>
     obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
@@ -134,14 +65,10 @@ theorem main [good_domain U] : ∃ f ∈ 𝓘 U, f '' U = ball (0 : ℂ) 1 := by
   obtain ⟨g, hg⟩ := step_2 U hz₀ ⟨f, hf.1.1, h5.2, mapsTo'.2 h10⟩ hfg
   exact ⟨g.to_fun, 𝓘_subset_𝓙 ⟨⟨g.is_diff, g.maps_to.mono_right ball_subset_closedBall⟩, g.is_inj⟩, hg⟩
 
-end RMT
-
-open RMT
-
 theorem RMT (h1 : IsOpen U) (h2 : IsConnected U) (h3 : U ≠ univ) (h4 : has_primitives U) :
     ∃ f : ℂ → ℂ, (DifferentiableOn ℂ f U) ∧ (InjOn f U) ∧ (f '' U = ball 0 1) := by
-  have : RMT.good_domain U := ⟨h1, h2.1, h2.2, h3, (h4.has_logs h1 h2.isPreconnected).has_sqrt⟩
-  obtain ⟨f, hf : f ∈ 𝓘 U, hfU⟩ := @RMT.main U _
+  have : good_domain U := ⟨h1, h2.1, h2.2, h3, (h4.has_logs h1 h2.isPreconnected).has_sqrt⟩
+  obtain ⟨f, hf : f ∈ 𝓘 U, hfU⟩ := main (U := U)
   exact ⟨f, hf.1.1, hf.2, hfU⟩
 
 #print axioms RMT

RMT4/Montel.lean

@@ -1,17 +1,13 @@
 import Mathlib.Analysis.Complex.Liouville
 import Mathlib.Topology.UniformSpace.Ascoli
-import RMT4.Basic
+import RMT4.Spaces
 import RMT4.defs
 import RMT4.hurwitz
 
 open Set Function Metric UniformConvergence Complex
 
 variable {ι : Type*} {U K : Set ℂ} {z : ℂ} {F : ι → 𝓒 U} {Q : Set ℂ → Set ℂ}
 
-@[simp] lemma union_compacts : ⋃₀ compacts U = U :=
-  subset_antisymm (λ _ ⟨_, hK, hz⟩ => hK.1 hz)
-    (λ z hz => ⟨{z}, ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩, mem_singleton z⟩)
-
 def UniformlyBoundedOn (F : ι → ℂ → ℂ) (U : Set ℂ) : Prop :=
   ∀ K ∈ compacts U, ∃ Q, IsCompact Q ∧ ∀ i, MapsTo (F i) K Q
 
@@ -61,22 +57,6 @@ lemma UniformlyBoundedOn.equicontinuousOn (h1 : UniformlyBoundedOn F U) (hU : Is
   convert mul_lt_mul' le_rfl this (norm_nonneg _) hMp
   field_simp [hMp.lt.ne.symm, mul_comm]
 
-def 𝓑 (U : Set ℂ) (Q : Set ℂ → Set ℂ) : Set (𝓒 U) :=
-    {f ∈ 𝓗 U | ∀ K ∈ compacts U, MapsTo f K (Q K)}
-
-lemma 𝓑_const {Q : Set ℂ} : 𝓑 U (fun _ => Q) = {f ∈ 𝓗 U | MapsTo f U Q} := by
-  simp [𝓑, ← mapsTo_sUnion]
-
-theorem isClosed_𝓑 (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) :
-    IsClosed (𝓑 U Q) := by
-  rw [𝓑, setOf_and] ; apply (isClosed_𝓗 hU).inter
-  simp only [setOf_forall, MapsTo]
-  apply isClosed_biInter ; intro K hK
-  apply isClosed_biInter ; intro z hz
-  apply (hQ K hK).isClosed.preimage
-  exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
-    (mem_singleton z) ⟨singleton_subset_iff.2 (hK.1 hz), isCompact_singleton⟩).continuous)
-
 theorem uniformlyBoundedOn_𝓑 (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) :
     UniformlyBoundedOn ((↑) : 𝓑 U Q → 𝓒 U) U := by
   exact fun K hK => ⟨Q K, hQ K hK, fun f => f.2.2 K hK⟩
@@ -99,3 +79,6 @@ theorem montel (hU : IsOpen U) (h1 : UniformlyBoundedOn F U) (h2 : ∀ i, Differ
   exact totallyBounded_subset l1 <| (isCompact_𝓑 hU hQ1).totallyBounded
 
 #print axioms montel
+
+lemma isCompact_𝓜 (hU : IsOpen U) : IsCompact (𝓜 U) := by
+  simpa only [𝓑_const] using isCompact_𝓑 hU (fun _ _ => isCompact_closedBall 0 1)

RMT4/Spaces.lean

@@ -0,0 +1,117 @@
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Analysis.Complex.OpenMapping
+import RMT4.defs
+
+open Topology Filter Set Function UniformConvergence Metric
+
+variable {U : Set ℂ} {Q : Set ℂ → Set ℂ} {ι : Type*} {l : Filter ι}
+
+-- `𝓒 U` is an alias for `ℂ → ℂ` equipped with compact convergence on `U`
+
+abbrev 𝓒 (U : Set ℂ) := ℂ →ᵤ[compacts U] ℂ
+
+noncomputable def uderiv (f : 𝓒 U) : 𝓒 U := deriv f
+
+lemma tendsto_𝓒_iff (hU : IsOpen U) {F : ι → 𝓒 U} {f : 𝓒 U} :
+    Tendsto F l (𝓝 f) ↔ TendstoLocallyUniformlyOn F f l U := by
+  simp [UniformOnFun.tendsto_iff_tendstoUniformlyOn, _root_.compacts]
+  exact (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).symm
+
+-- `𝓗 U` is the space of holomorphic functions on `U`
+
+def 𝓗 (U : Set ℂ) := {f : 𝓒 U | DifferentiableOn ℂ f U}
+
+lemma isClosed_𝓗 (hU : IsOpen U) : IsClosed (𝓗 U) := by
+  refine isClosed_iff_clusterPt.2 (λ f hf => ?_)
+  refine @TendstoLocallyUniformlyOn.differentiableOn _ _ _ _ _ _ _ id f hf ?_ ?_ hU
+  · simp [← tendsto_𝓒_iff hU, Tendsto]
+  · simp [eventually_inf_principal, 𝓗]; exact eventually_of_forall (λ g => id)
+
+lemma ContinuousOn_uderiv (hU : IsOpen U) : ContinuousOn uderiv (𝓗 U) := by
+  rintro f -
+  refine (tendsto_𝓒_iff hU).2 ?_
+  refine TendstoLocallyUniformlyOn.deriv ?_ eventually_mem_nhdsWithin hU
+  apply (tendsto_𝓒_iff hU).1
+  exact nhdsWithin_le_nhds
+
+-- `𝓑 U Q` is the collection of `Q`-bounded holomorphic maps on `U`
+
+def 𝓑 (U : Set ℂ) (Q : Set ℂ → Set ℂ) : Set (𝓒 U) :=
+    {f ∈ 𝓗 U | ∀ K ∈ compacts U, MapsTo f K (Q K)}
+
+lemma 𝓑_const {Q : Set ℂ} : 𝓑 U (fun _ => Q) = {f ∈ 𝓗 U | MapsTo f U Q} := by
+  simp [𝓑, ← mapsTo_sUnion]
+
+theorem isClosed_𝓑 (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) :
+    IsClosed (𝓑 U Q) := by
+  rw [𝓑, setOf_and] ; apply (isClosed_𝓗 hU).inter
+  simp only [setOf_forall, MapsTo]
+  apply isClosed_biInter ; intro K hK
+  apply isClosed_biInter ; intro z hz
+  apply (hQ K hK).isClosed.preimage
+  exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
+    (mem_singleton z) ⟨singleton_subset_iff.2 (hK.1 hz), isCompact_singleton⟩).continuous)
+
+-- `𝓜 U` : holomorphic functions to the unit closed ball
+
+def 𝓜 (U : Set ℂ) := {f ∈ 𝓗 U | MapsTo f U (closedBall (0 : ℂ) 1)}
+
+lemma 𝓜_eq_𝓑 : 𝓜 U = 𝓑 U (fun _ => closedBall 0 1) := 𝓑_const.symm
+
+lemma IsClosed_𝓜 (hU : IsOpen U) : IsClosed (𝓜 U) := by
+  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)
+    (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous)
+
+-- `𝓘 U` : holomorphic injections into the unit ball
+
+def 𝓘 (U : Set ℂ) := {f ∈ 𝓜 U | InjOn f U}
+
+lemma 𝓘_nonempty [good_domain U] : (𝓘 U).Nonempty := by
+  obtain ⟨u, hu⟩ := nonempty_compl.mpr (good_domain.ne_univ : U ≠ univ)
+  let f : ℂ → ℂ := λ z => z - u
+  have f_inj : Injective f := λ _ _ h => sub_left_inj.mp h
+  have f_hol : DifferentiableOn ℂ f U := differentiableOn_id.sub (differentiableOn_const u)
+  have f_noz : ∀ ⦃z : ℂ⦄, z ∈ U -> f z ≠ 0 := λ z hz f0 => hu (sub_eq_zero.mp f0 ▸ hz)
+
+  obtain ⟨g, g_hol, g_sqf⟩ := good_domain.has_sqrt f f_noz f_hol
+  obtain ⟨z₀, hz₀⟩ := (good_domain.is_nonempty : U.Nonempty)
+
+  have gU_nhd : g '' U ∈ 𝓝 (g z₀) := by
+    have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
+    have e2 := g_hol.analyticAt e1
+    have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
+    have dg_nonzero : deriv g z₀ ≠ 0 := by
+      have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
+      simp [e3, deriv_sub_const, f]
+      intro h
+      have := g_sqf hz₀
+      rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
+      cases f_noz hz₀ this
+    refine e2.eventually_constant_or_nhds_le_map_nhds.resolve_left (λ h => ?_) (image_mem_map e1)
+    simp [EventuallyEq.deriv_eq h] at dg_nonzero
+
+  obtain ⟨r, r_pos, hr⟩ := Metric.mem_nhds_iff.mp gU_nhd
+  let gg : embedding U ((closedBall (- g z₀) (r / 2))ᶜ) :=
+  { to_fun := g,
+    is_diff := g_hol,
+    is_inj := λ z₁ hz₁ z₂ hz₂ hgz => f_inj (by simp [g_sqf _, hz₁, hz₂, hgz]),
+    maps_to := λ z hz hgz => by {
+      apply f_noz hz
+      rw [mem_closed_ball_neg_iff_mem_neg_closed_ball] at hgz
+      obtain ⟨z', hz', hgz'⟩ := (closedBall_subset_ball (by linarith)).trans hr hgz
+      have hzz' : z = z' := f_inj (by simp [g_sqf hz, g_sqf hz', hgz'])
+      simpa [hzz', neg_eq_self_iff, g_sqf hz'] using hgz'.symm } }
+
+  let ggg := (embedding.inv _ (by linarith)).comp gg
+  refine ⟨ggg.to_fun, ⟨ggg.is_diff, ?_⟩, ggg.is_inj⟩
+  exact λ z hz => ball_subset_closedBall (ggg.maps_to hz)
+
+-- `𝓙 U` : the closure of `𝓘 U`, injections and constants
+
+def 𝓙 (U : Set ℂ) := {f ∈ 𝓜 U | InjOn f U ∨ ∃ w : ℂ, EqOn f (λ _ => w) U}
+
+lemma 𝓘_subset_𝓙 : 𝓘 U ⊆ 𝓙 U := λ _ hf => ⟨hf.1, Or.inl hf.2⟩

RMT4/defs.lean

@@ -1,12 +1,15 @@
 import RMT4.to_mathlib
 import RMT4.deriv_inj
-import RMT4.Basic
 
 open Complex Metric Set
 
 variable {u : ℂ} {U V W : Set ℂ}
 
-namespace RMT
+def compacts (U : Set ℂ) : Set (Set ℂ) := {K ⊆ U | IsCompact K}
+
+@[simp] lemma union_compacts : ⋃₀ compacts U = U :=
+  subset_antisymm (λ _ ⟨_, hK, hz⟩ => hK.1 hz)
+    (λ z hz => ⟨{z}, ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩, mem_singleton z⟩)
 
 def 𝔻 : Set ℂ := ball 0 1
 
@@ -88,5 +91,3 @@ noncomputable def embedding.inv (w : ℂ) {r : ℝ} (hr : 0 < r) : embedding ((c
 lemma embedding.deriv_ne_zero {f : embedding U V} {z : ℂ} (hU : IsOpen U) (hz : z ∈ U) :
   deriv f z ≠ 0 :=
 deriv_ne_zero_of_inj hU f.is_diff f.is_inj hz
-
-end RMT

RMT4/etape2.lean

@@ -4,8 +4,6 @@ import RMT4.to_mathlib
 
 open Complex ComplexConjugate Set Metric Topology Filter
 
-namespace RMT
-
 variable {z u z₀ : ℂ} (U : Set ℂ) [good_domain U]
 
 lemma one_sub_mul_conj_ne_zero (hu : u ∈ 𝔻) (hz : z ∈ 𝔻) : 1 - z * conj u ≠ 0 := by
@@ -174,5 +172,3 @@ lemma step_2 (hz₀ : z₀ ∈ U) (f : embedding U 𝔻) (hf : f '' U ⊂ 𝔻)
       · intro h
         have := (φ v_in_𝔻).is_inj e1 e2 h
         norm_num at this
-
-end RMT