From 3f2407241274c384abcd006b2f43ca1e487f4462 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 28 Nov 2024 18:57:43 +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/meromorphicOn_divisor.lean         | 23 +++++++++++++++++++
 Nevanlinna/stronglyMeromorphicOn.lean         |  4 ++--
 .../stronglyMeromorphicOn_eliminate.lean      | 23 +++++++++++--------
 3 files changed, 39 insertions(+), 11 deletions(-)

diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index 532a372..2e7ba1b 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -159,3 +159,26 @@ theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn
     apply MeromorphicAt.order_congr
     exact EventuallyEq.symm (makeStronglyMeromorphicOn_changeDiscrete hf hz)
   · simp [hz]
+
+
+
+/- Strongly MeromorphicOn of non-negative order is analytic -/
+theorem StronglyMeromorphicOn.analyticOnNhd
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ h₁f.meromorphicOn.divisor x) :
+  AnalyticOnNhd ℂ f U := by
+
+  apply StronglyMeromorphicOn.analytic
+  intro z hz
+  let A := h₂f z hz
+  unfold MeromorphicOn.divisor at A
+  simp [hz] at A
+  by_cases h : (h₁f z hz).meromorphicAt.order = ⊤
+  · rw [h]
+    simp
+  · rw [WithTop.le_untop'_iff] at A
+    tauto
+    tauto
+  assumption
diff --git a/Nevanlinna/stronglyMeromorphicOn.lean b/Nevanlinna/stronglyMeromorphicOn.lean
index 2eb2420..8ef4846 100644
--- a/Nevanlinna/stronglyMeromorphicOn.lean
+++ b/Nevanlinna/stronglyMeromorphicOn.lean
@@ -26,8 +26,8 @@ theorem StronglyMeromorphicOn.analytic
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
-  ∀ z ∈ U, AnalyticAt ℂ f z := by
+  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order) :
+  AnalyticOnNhd ℂ f U := by
   intro z hz
   apply StronglyMeromorphicAt.analytic
   exact h₂f z hz
diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index 54d9488..6273835 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -324,8 +324,7 @@ theorem MeromorphicOn.decompose₃
     · apply AnalyticAt.analyticWithinAt
       rw [analyticAt_of_mul_analytic]
 
-
-    sorry
+      sorry
 
   have h₂h : StronglyMeromorphicOn h U := by
     sorry
@@ -383,8 +382,8 @@ theorem MeromorphicOn.decompose₃'
     exact (StronglyMeromorphicOn.meromorphicOn h₁f).divisor.supportInU
   have h₃h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order ≠ ⊤ := by
     intro z hz
+    apply stronglyMeromorphicOn_ratlPolynomial₃order
 
-    sorry
   let g' := f * h₁
   have h₁g' : MeromorphicOn g' U := h₁f.meromorphicOn.mul h₁h₁.meromorphicOn
   have h₂g' : h₁g'.divisor.toFun = 0 := by
@@ -394,20 +393,26 @@ theorem MeromorphicOn.decompose₃'
     simp
 
   let g := h₁g'.makeStronglyMeromorphicOn
-  have h₁g : StronglyMeromorphicOn g U := by
-    sorry
+  have h₁g : StronglyMeromorphicOn g U := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁g'
   have h₂g : h₁g.meromorphicOn.divisor.toFun = 0 := by
-    sorry
-  have h₃g : AnalyticOn ℂ g U := by
-    sorry
+    rw [← MeromorphicOn.divisor_of_makeStronglyMeromorphicOn]
+    rw [h₂g']
+  have h₃g : AnalyticOnNhd ℂ g U := by
+    apply StronglyMeromorphicOn.analyticOnNhd
+    rw [h₂g]
+    simp
+    assumption
   have h₄g : ∀ u : U, g u ≠ 0 := by
+    intro u
+    rw [← (h₁g u.1 u.2).order_eq_zero_iff]
+
     sorry
 
   use g
   constructor
   · exact StronglyMeromorphicOn.meromorphicOn h₁g
   · constructor
-    · exact h₃g
+    · exact AnalyticOnNhd.analyticOn h₃g
     · constructor
       · exact h₄g
       · sorry