From f4d035100247c1d737fc48c4f4a0601064a41af9 Mon Sep 17 00:00:00 2001 From: Vincent Beffara Date: Mon, 18 Mar 2024 14:45:22 +0100 Subject: [PATCH] Tweaks --- RMT4.lean | 18 ++---------------- RMT4/Basic.lean | 17 ++++++++++++++--- RMT4/hurwitz.lean | 4 ++-- RMT4/montel.lean | 8 ++++---- 4 files changed, 22 insertions(+), 25 deletions(-) diff --git a/RMT4.lean b/RMT4.lean index 1952511..376ad8b 100644 --- a/RMT4.lean +++ b/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 _ diff --git a/RMT4/Basic.lean b/RMT4/Basic.lean index 757b633..c344134 100644 --- a/RMT4/Basic.lean +++ b/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 diff --git a/RMT4/hurwitz.lean b/RMT4/hurwitz.lean index c56dc36..22e7e47 100644 --- a/RMT4/hurwitz.lean +++ b/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) := diff --git a/RMT4/montel.lean b/RMT4/montel.lean index 401aba4..6846891 100644 --- a/RMT4/montel.lean +++ b/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⟩