From a8ab8a5875fcca99e44e033e50fdcdf40457fa2f Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 11 Nov 2024 16:50:49 +0100 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/analyticAt.lean | 24 ++++++++ Nevanlinna/meromorphicAt.lean | 21 +++++++ Nevanlinna/meromorphicOn_decompose.lean | 7 +++ Nevanlinna/stronglyMeromorphicAt.lean | 82 ++++++++++++------------- 4 files changed, 92 insertions(+), 42 deletions(-) diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean index b9c6693..263e0db 100644 --- a/Nevanlinna/analyticAt.lean +++ b/Nevanlinna/analyticAt.lean @@ -2,6 +2,8 @@ import Mathlib.Analysis.Analytic.IsolatedZeros import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Analytic.Linear +open Topology + theorem AnalyticAt.order_neq_top_iff {f : ℂ → ℂ} @@ -236,3 +238,25 @@ theorem AnalyticAt.order_comp_CLE rw [this] simp + + +theorem AnalyticAt.localIdentity + {f g : ℂ → ℂ} + {z₀ : ℂ} + (hf : AnalyticAt ℂ f z₀) + (hg : AnalyticAt ℂ g z₀) : + f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by + intro h + let Δ := f - g + have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg + have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by + exact Filter.eventuallyEq_iff_sub.mp h + + have : Δ =ᶠ[𝓝 z₀] 0 := by + rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h + · exact h + · have := Filter.EventuallyEq.eventually t₁ + let A := Filter.eventually_and.2 ⟨this, h⟩ + let _ := Filter.Eventually.exists A + tauto + exact Filter.eventuallyEq_iff_sub.mpr this diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index c7f09f0..1f9d557 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/Nevanlinna/meromorphicAt.lean @@ -52,3 +52,24 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero · constructor · exact h₂N · exact h₃N + +theorem MeromorphicAt.order_congr + {f₁ f₂ : ℂ → ℂ} + {z₀ : ℂ} + (hf₁ : MeromorphicAt f₁ z₀) + (h : f₁ =ᶠ[𝓝[≠] z₀] f₂): + hf₁.order = (hf₁.congr h).order := by + by_cases hord : hf₁.order = ⊤ + · rw [hord, eq_comm] + rw [hf₁.order_eq_top_iff] at hord + rw [(hf₁.congr h).order_eq_top_iff] + exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h)) + · obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord + obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn + rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff] + use g + constructor + · assumption + · constructor + · assumption + · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h)) diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean index e9a0b0b..bc04777 100644 --- a/Nevanlinna/meromorphicOn_decompose.lean +++ b/Nevanlinna/meromorphicOn_decompose.lean @@ -24,6 +24,7 @@ lemma WithTopCoe rw [this] rfl + theorem MeromorphicOn.decompose {f : ℂ → ℂ} {U : Set ℂ} @@ -70,5 +71,11 @@ theorem MeromorphicOn.decompose rw [hn] exact A · intro z hz + have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by + sorry + have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by + sorry + have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by + sorry sorry diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 4f24a1a..bb65ec0 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -1,6 +1,7 @@ import Mathlib.Analysis.Analytic.Meromorphic import Nevanlinna.analyticAt import Nevanlinna.mathlibAddOn +import Nevanlinna.meromorphicAt open Topology @@ -13,6 +14,7 @@ def StronglyMeromorphicAt (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z)) + /- Strongly MeromorphicAt is Meromorphic -/ theorem StronglyMeromorphicAt.meromorphicAt {f : ℂ → ℂ} @@ -122,6 +124,42 @@ theorem stronglyMeromorphicAt_congr assumption +theorem StronglyMeromorphicAt.order_eq_zero_iff + {f : ℂ → ℂ} + {z₀ : ℂ} + (hf : StronglyMeromorphicAt f z₀) : + hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by + sorry + +theorem StronglyMeromorphicAt.localIdentity + {f g : ℂ → ℂ} + {z₀ : ℂ} + (hf : StronglyMeromorphicAt f z₀) + (hg : StronglyMeromorphicAt g z₀) : + f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by + + intro h + + have t₀ : hf.meromorphicAt.order = hg.meromorphicAt.order := by + exact hf.meromorphicAt.order_congr h + + by_cases cs : hf.meromorphicAt.order = 0 + · rw [cs] at t₀ + have h₁f := hf.analytic (le_of_eq (id (Eq.symm cs))) + have h₁g := hg.analytic (le_of_eq t₀) + exact h₁f.localIdentity h₁g h + · apply Mnhds h + let A := cs + rw [hf.order_eq_zero_iff] at A + simp at A + let B := cs + rw [t₀] at B + rw [hg.order_eq_zero_iff] at B + simp at B + rw [A, B] + + + /- Make strongly MeromorphicAt -/ noncomputable def MeromorphicAt.makeStronglyMeromorphicAt {f : ℂ → ℂ} @@ -155,46 +193,6 @@ lemma m₂ apply eventually_nhdsWithin_of_forall exact fun x a => m₁ hf x a -/- -lemma Mnhds - {f g : ℂ → ℂ} - {z₀ : ℂ} - (h₁ : f =ᶠ[𝓝[≠] z₀] g) - (h₂ : f z₀ = g z₀) : - f =ᶠ[𝓝 z₀] g := by - apply eventually_nhds_iff.2 - obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁) - use t - constructor - · intro y hy - by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ) - · exact h₁t y hy h₂y - · simp at h₂y - rwa [h₂y] - · exact h₂t --/ - -theorem localIdentity - {f g : ℂ → ℂ} - {z₀ : ℂ} - (hf : AnalyticAt ℂ f z₀) - (hg : AnalyticAt ℂ g z₀) : - f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by - intro h - let Δ := f - g - have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg - have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by - exact Filter.eventuallyEq_iff_sub.mp h - - have : Δ =ᶠ[𝓝 z₀] 0 := by - rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h - · exact h - · have := Filter.EventuallyEq.eventually t₁ - let A := Filter.eventually_and.2 ⟨this, h⟩ - let _ := Filter.Eventually.exists A - tauto - exact Filter.eventuallyEq_iff_sub.mpr this - theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic {f : ℂ → ℂ} @@ -240,7 +238,7 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic rw [hn] at h₃g; simp at h₃g simp have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by - apply localIdentity h₁g h₁G + apply h₁g.localIdentity h₁G exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G rw [Filter.EventuallyEq.eq_of_nhds this] · have : hf.order ≠ 0 := h₃f @@ -292,7 +290,7 @@ theorem makeStronglyMeromorphic_id let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀ have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec A - apply localIdentity h₁g h₀ + apply h₁g.localIdentity h₀ rw [hn] at h₃g simp at h₃g simp at h₂