Tweaks

RMT4.lean

@@ -25,20 +25,6 @@ variable {ι : Type*} {l : Filter ι} {U : Set ℂ} {z₀ : ℂ}
 
 namespace RMT
 
-noncomputable def uderiv (f : ℂ →ᵤ[compacts U] ℂ) : ℂ →ᵤ[compacts U] ℂ := deriv f
-
-lemma ContinuousOn_uderiv (hU : IsOpen U) : ContinuousOn uderiv (𝓗 U) := by
-  rintro f hf
-  haveI := nhdsWithin_neBot_of_mem hf
-  refine (tendsto_iff hU).2 ?_
-  refine TendstoLocallyUniformlyOn.deriv ?_ ?_ hU
-  · apply (tendsto_iff hU).1
-    exact nhdsWithin_le_nhds
-  · rw [eventually_nhdsWithin_iff]
-    apply eventually_of_forall
-    intro f hf
-    exact hf
-
 -- `𝓜 U` : holomorphic functions to the unit closed ball
 
 def 𝓜 (U : Set ℂ) := {f ∈ 𝓗 U | MapsTo f U (closedBall (0 : ℂ) 1)}
@@ -49,7 +35,7 @@ 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 : ℂ →ᵤ[compacts U] ℂ | MapsTo f U (closedBall 0 1)}
+  suffices h : IsClosed {f : 𝓒 U | MapsTo f U (closedBall 0 1)}
   · exact (isClosed_𝓗 hU).inter h
   simp_rw [MapsTo, setOf_forall]
   refine isClosed_biInter (λ z hz => isClosed_ball.preimage ?_)
@@ -132,7 +118,7 @@ lemma IsCompact_𝓙 [good_domain U] : IsCompact (𝓙 U) := by
 
 -- The proof
 
-noncomputable def obs (z₀ : ℂ) (f : ℂ →ᵤ[compacts U] ℂ) : ℝ := ‖deriv f z₀‖
+noncomputable def obs (z₀ : ℂ) (f : 𝓒 U) : ℝ := ‖deriv f z₀‖
 
 lemma ContinuousOn_obs (hU : IsOpen U) (hz₀ : z₀ ∈ U) : ContinuousOn (obs z₀) (𝓗 U) := by
   have e1 : z₀ ∈ {z₀} := mem_singleton _

RMT4/Basic.lean

@@ -5,11 +5,15 @@ open Topology Filter Set Function UniformConvergence
 
 variable {ι : Type*} {l : Filter ι} {U : Set ℂ}
 
-def compacts (U : Set ℂ) : Set (Set ℂ) := {K | K ⊆ U ∧ IsCompact K}
+def compacts (U : Set ℂ) : Set (Set ℂ) := {K ⊆ U | IsCompact K}
 
-def 𝓗 (U : Set ℂ) := {f : ℂ →ᵤ[compacts U] ℂ | DifferentiableOn ℂ f U}
+abbrev 𝓒 (U : Set ℂ) := ℂ →ᵤ[compacts U] ℂ
 
-lemma tendsto_iff (hU : IsOpen U) {F : ι → ℂ →ᵤ[compacts U] ℂ} {f : ℂ →ᵤ[compacts U] ℂ} :
+noncomputable def uderiv (f : 𝓒 U) : 𝓒 U := deriv f
+
+def 𝓗 (U : Set ℂ) := {f : 𝓒 U | DifferentiableOn ℂ f U}
+
+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
@@ -19,3 +23,10 @@ lemma isClosed_𝓗 (hU : IsOpen U) : IsClosed (𝓗 U) := by
   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

RMT4/hurwitz.lean

@@ -16,8 +16,8 @@ lemma mem_iff_eventually_subset (hp : p.HasBasis (λ t : ℝ => 0 < t) φ) (hφ
     λ h => h ⟨Eq.le (abs_eq_self.mpr hε.le), hε⟩⟩)
 
 lemma eventually_nhds_iff_eventually_ball [PseudoMetricSpace α] :
-  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
-mem_iff_eventually_subset nhds_basis_ball (λ _ _ => ball_subset_ball)
+    (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
+  mem_iff_eventually_subset nhds_basis_ball (λ _ _ => ball_subset_ball)
 
 lemma eventually_nhds_iff_eventually_closed_ball [PseudoMetricSpace α] :
   (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, P z) :=

RMT4/montel.lean

@@ -6,7 +6,7 @@ import RMT4.hurwitz
 
 open Set Function Metric UniformConvergence Complex
 
-variable {ι : Type*} {U K : Set ℂ} {z : ℂ} {F : ι → ℂ →ᵤ[compacts U] ℂ} {Q : Set ℂ → Set ℂ}
+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)
@@ -61,7 +61,7 @@ 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 (ℂ →ᵤ[compacts 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
@@ -78,12 +78,12 @@ theorem isClosed_𝓑 (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K
     (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 → ℂ →ᵤ[compacts U] ℂ) U := by
+    UniformlyBoundedOn ((↑) : 𝓑 U Q → 𝓒 U) U := by
   exact fun K hK => ⟨Q K, hQ K hK, fun f => f.2.2 K hK⟩
 
 theorem isCompact_𝓑 (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) :
     IsCompact (𝓑 U Q) := by
-  have l1 (K) (hK : K ∈ compacts U) : EquicontinuousOn ((↑) : 𝓑 U Q → ℂ →ᵤ[compacts U] ℂ) K :=
+  have l1 (K) (hK : K ∈ compacts U) : EquicontinuousOn ((↑) : 𝓑 U Q → 𝓒 U) K :=
     (uniformlyBoundedOn_𝓑 hQ).equicontinuousOn hU (fun f => f.2.1) hK
   have l2 (K) (hK : K ∈ compacts U) (x) (hx : x ∈ K) : ∃ L, IsCompact L ∧ ∀ i : 𝓑 U Q, i.1 x ∈ L :=
     ⟨Q K, hQ K hK, fun f => f.2.2 K hK hx⟩