From 226609f9c0dfa17a12cb52733bc23ca7a04a3e6d Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 19 Nov 2024 08:45:20 +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/meromorphicAt.lean | 3 +++ Nevanlinna/stronglyMeromorphicOn_eliminate.lean | 14 +++++++++++--- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index 942675e..516f4bf 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/Nevanlinna/meromorphicAt.lean @@ -145,3 +145,6 @@ theorem MeromorphicAt.order_mul · constructor · exact IsOpen.inter h₂t₁ h₂t₂ · exact Set.mem_inter h₃t₁ h₃t₂ + + +-- might want theorem MeromorphicAt.order_zpow diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index 632938f..55977ca 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -30,9 +30,17 @@ theorem MeromorphicOn.decompose₁ apply AnalyticOnNhd.sub exact analyticOnNhd_id exact analyticOnNhd_const - have h₂h₁ : (h₁h₁ z₀ hz₀).order = -h₁f.divisor z₀ := by - - sorry + let n : ℤ := (-h₁f.divisor z₀) + have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by + simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff] + use 1 + constructor + · apply analyticAt_const + · constructor + · simp + · apply eventually_nhdsWithin_of_forall + intro z hz + simp let g₁ := f * h₁ have h₁g₁ : MeromorphicOn g₁ U := by