From 971b7cc23c346f953c8ae079b0a93a4047044b7a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 19 Nov 2024 15:54:28 +0100 Subject: [PATCH] Working! --- Nevanlinna/analyticAt.lean | 34 +++++++ Nevanlinna/stronglyMeromorphicAt.lean | 4 +- .../stronglyMeromorphicOn_eliminate.lean | 96 ++++++++++++++++--- 3 files changed, 121 insertions(+), 13 deletions(-) diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean index 87731af..d1895ae 100644 --- a/Nevanlinna/analyticAt.lean +++ b/Nevanlinna/analyticAt.lean @@ -308,3 +308,37 @@ theorem AnalyticAt.zpow intro x rw [zpow_neg] exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f) + + +/- A function is analytic at a point iff it is analytic after multiplication + with a non-vanishing analytic function +-/ +theorem analyticAt_of_mul_analytic + {f g : ℂ → ℂ} + {z₀ : ℂ} + (h₁g : AnalyticAt ℂ g z₀) + (h₂g : g z₀ ≠ 0) : + AnalyticAt ℂ f z₀ ↔ AnalyticAt ℂ (f * g) z₀ := by + constructor + · exact fun a => AnalyticAt.mul₁ a h₁g + · intro hprod + + let g' := fun z ↦ (g z)⁻¹ + have h₁g' := h₁g.inv h₂g + have h₂g' : g' z₀ ≠ 0 := by + exact inv_ne_zero h₂g + + have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by + unfold Filter.EventuallyEq + apply Filter.eventually_iff_exists_mem.mpr + use g⁻¹' {0}ᶜ + constructor + · apply ContinuousAt.preimage_mem_nhds + exact AnalyticAt.continuousAt h₁g + exact compl_singleton_mem_nhds_iff.mpr h₂g + · intro y hy + simp at hy + simp [hy] + rw [analyticAt_congr this] + apply hprod.mul + exact h₁g' diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 5ee3ec0..e2a8d95 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -169,7 +169,9 @@ theorem stronglyMeromorphicAt_congr · apply Filter.EventuallyEq.trans hfg assumption - +/- A function is strongly meromorphic at a point iff it is strongly meromorphic + after multiplication with a non-vanishing analytic function +-/ theorem stronglyMeromorphicAt_of_mul_analytic {f g : ℂ → ℂ} {z₀ : ℂ} diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index 46ccb52..f7aac4b 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -170,12 +170,7 @@ theorem MeromorphicOn.decompose₂ intro hOrder obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀, h₄g₀⟩ := iHyp (fun p hp ↦ hOrder p (Finset.mem_insert_of_mem hp)) - have h₅g₀ : StronglyMeromorphicAt g₀ u := by - - rw [stronglyMeromorphicAt_of_mul_analytic (g := ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) (z₀ := u) (f := g₀)] - rw [← h₄g₀] - exact hf u u.2 - -- + have h₀ : AnalyticAt ℂ (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u := by have : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) = (fun z => ∏ p : P, (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by funext w simp @@ -186,14 +181,14 @@ theorem MeromorphicOn.decompose₂ apply AnalyticAt.sub apply analyticAt_id apply analyticAt_const - -- by_contra hCon rw [sub_eq_zero] at hCon have : p.1 = u := by exact SetCoe.ext (_root_.id (Eq.symm hCon)) rw [← this] at hu simp [hp] at hu - -- + + have h₁ : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u ≠ 0 := by simp only [Finset.prod_apply] rw [Finset.prod_ne_zero_iff] intro p hp @@ -205,16 +200,93 @@ theorem MeromorphicOn.decompose₂ rw [← this] at hu simp [hp] at hu + have h₅g₀ : StronglyMeromorphicAt g₀ u := by + rw [stronglyMeromorphicAt_of_mul_analytic h₀ h₁] + rw [← h₄g₀] + exact hf u u.2 have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by - sorry + by_contra hCon + let A := (h₁g₀ u u.2).order_mul h₀.meromorphicAt + simp_rw [← h₄g₀, hCon] at A + simp at A + let B := hOrder u (Finset.mem_insert_self u P) + tauto obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁g₀.decompose₁ h₅g₀ h₆g₀ u.2 use g · constructor · exact h₁g · constructor - · sorry + · intro ⟨v₁, v₂⟩ + simp + simp at v₂ + rcases v₂ with hv|hv + · rwa [hv] + · let A := h₂g₀ ⟨v₁, hv⟩ + rw [h₄g] at A + rw [← analyticAt_of_mul_analytic] at A + simp at A + exact A + -- + simp + apply AnalyticAt.zpow + apply AnalyticAt.sub + apply analyticAt_id + apply analyticAt_const + by_contra hCon + rw [sub_eq_zero] at hCon + + have : v₁ = u := by + exact SetCoe.ext hCon + rw [this] at hv + tauto + -- + apply zpow_ne_zero + simp + by_contra hCon + rw [sub_eq_zero] at hCon + have : v₁ = u := by + exact SetCoe.ext hCon + rw [this] at hv + tauto + · constructor - · sorry - · sorry + · intro ⟨v₁, v₂⟩ + simp + simp at v₂ + rcases v₂ with hv|hv + · rwa [hv] + · by_contra hCon + let A := h₃g₀ ⟨v₁,hv⟩ + rw [h₄g] at A + simp at A + tauto + · conv => + left + rw [h₄g₀, h₄g] + simp + rw [mul_assoc] + congr + rw [Finset.prod_insert] + simp + congr + have : (hf u u.2).meromorphicAt.order = (h₁g₀ u u.2).order := by + have h₅g₀ : f =ᶠ[𝓝 u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by + exact Eq.eventuallyEq h₄g₀ + have h₆g₀ : f =ᶠ[𝓝[≠] u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by + exact eventuallyEq_nhdsWithin_of_eqOn fun ⦃x⦄ a => congrFun h₄g₀ x + rw [(hf u u.2).meromorphicAt.order_congr h₆g₀] + let C := (h₁g₀ u u.2).order_mul h₀.meromorphicAt + rw [C] + let D := h₀.order_eq_zero_iff.2 h₁ + let E := h₀.meromorphicAt_order + rw [E, D] + simp + have : hf.meromorphicOn.divisor u = h₁g₀.divisor u := by + unfold MeromorphicOn.divisor + simp + rw [this] + rw [this] + -- + simpa