From 8bc84748a32b70216e806241def3f00388d4b709 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 28 Nov 2024 16:52:56 +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.lean                 | 36 +++++++++++-----
 .../stronglyMeromorphicOn_ratlPolynomial.lean | 42 ++++++++++++++++---
 2 files changed, 62 insertions(+), 16 deletions(-)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index 3e99437..94bef60 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -105,14 +105,15 @@ theorem MeromorphicOn.clopen_of_order_eq_top
   · exact open_of_order_eq_top h₁f
 
 
-theorem MeromorphicOn.order_ne_top
+theorem MeromorphicOn.order_ne_top'
+  {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsConnected U)
-  (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ u : U, f u ≠ 0) :
-  ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) :
+  ∀ u : U, (h₁f u u.2).order ≠ ⊤ := by
 
-  let A := h₁f.meromorphicOn.clopen_of_order_eq_top
+  let A := h₁f.clopen_of_order_eq_top
   have : PreconnectedSpace U := by
     apply isPreconnected_iff_preconnectedSpace.mp
     exact IsConnected.isPreconnected hU
@@ -123,9 +124,24 @@ theorem MeromorphicOn.order_ne_top
     rw [← h] at this
     simp at this
     tauto
-  · obtain ⟨u, hu⟩ := h₂f
-    have : u ∈ (Set.univ : Set U) := by trivial
-    rw [← h] at this
-    simp at this
-    rw [(h₁f u u.2).order_eq_zero_iff.2 hu] at this
+  · obtain ⟨u, hU⟩ := h₂f
+    have A : u ∈ Set.univ := by trivial
+    rw [← h] at A
+    simp at A
     tauto
+
+
+theorem MeromorphicOn.order_ne_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsConnected U)
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∃ u : U, f u ≠ 0) :
+  ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
+
+  apply MeromorphicOn.order_ne_top' hU h₁f.meromorphicOn
+  obtain ⟨u, hu⟩ := h₂f
+  use u
+  rw [← (h₁f u u.2).order_eq_zero_iff] at hu
+  rw [hu]
+  simp
diff --git a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
index 1e169c6..005f635 100644
--- a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
@@ -1,4 +1,5 @@
 import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.meromorphicOn
 import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.mathlibAddOn
 
@@ -61,12 +62,6 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃
     apply AnalyticOn.stronglyMeromorphicOn
     apply analyticOnNhd_const
 
-theorem stronglyMeromorphicOn_ratlPolynomial₃U
-  (d : ℂ → ℤ)
-  (U : Set ℂ) :
-  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
-  intro z hz
-  exact stronglyMeromorphicOn_ratlPolynomial₃ d z trivial
 
 
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
@@ -140,6 +135,40 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
         simp
 
 
+theorem stronglyMeromorphicOn_ratlPolynomial₃order
+  {z : ℂ}
+  (d : ℂ → ℤ) :
+  ((stronglyMeromorphicOn_ratlPolynomial₃ d) z trivial).meromorphicAt.order ≠ ⊤ := by
+
+  have h₂d : (Function.mulSupport fun u z ↦ (z - u) ^ d u) = d.support := by
+    ext u
+    constructor
+    · intro h
+      simp at h
+      simp
+      by_contra hCon
+      rw [hCon] at h
+      simp at h
+      tauto
+    · intro h
+      simp
+      by_contra hCon
+      let A := congrFun hCon u
+      simp at A
+      have t₁ : (0 : ℂ) ^ d u ≠ 0 := ne_zero_of_eq_one A
+      rw [zpow_ne_zero_iff h] at t₁
+      tauto
+
+  by_cases hd : Set.Finite (Function.support d)
+  · rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d hd]
+    simp
+  · rw [← h₂d] at hd
+    have : (Function.mulSupport fun u z => (z - u) ^ d u).Infinite := by
+      exact hd
+    simp_rw [finprod_of_infinite_mulSupport this]
+    sorry
+
+
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial
   (d : ℂ → ℤ)
   (h₁d : Set.Finite d.support) :
@@ -150,6 +179,7 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial
   rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d h₁d]
   simp
 
+
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial_U
   {U : Set ℂ}
   (d : ℂ → ℤ)