From ab02fe715ea94b21cbccf9a182e3827d3692dacf Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 19 Nov 2024 13:57:08 +0100 Subject: [PATCH] Update stronglyMeromorphicOn_eliminate.lean --- .../stronglyMeromorphicOn_eliminate.lean | 35 ++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index faf009c..46ccb52 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -172,7 +172,40 @@ theorem MeromorphicOn.decompose₂ have h₅g₀ : StronglyMeromorphicAt g₀ u := by - sorry + 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 : (∏ 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 + rw [this] + apply Finset.analyticAt_prod + intro p hp + apply AnalyticAt.zpow + 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 + -- + simp only [Finset.prod_apply] + rw [Finset.prod_ne_zero_iff] + intro p hp + apply zpow_ne_zero + 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₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by sorry