From b038a5f47fe202992b17bb0cd3dc3104aad3d405 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 20 Nov 2024 16:08:59 +0100
Subject: [PATCH] Update stronglyMeromorphicOn.lean

---
 Nevanlinna/stronglyMeromorphicOn.lean | 77 ++++++++++++++++++++++++---
 1 file changed, 71 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphicOn.lean b/Nevanlinna/stronglyMeromorphicOn.lean
index ae7ee49..0a34c95 100644
--- a/Nevanlinna/stronglyMeromorphicOn.lean
+++ b/Nevanlinna/stronglyMeromorphicOn.lean
@@ -1,5 +1,5 @@
 import Nevanlinna.stronglyMeromorphicAt
-
+import Mathlib.Algebra.BigOperators.Finprod
 
 open Topology
 
@@ -79,12 +79,77 @@ theorem makeStronglyMeromorphicOn_changeDiscrete
     · simp [h₂v]
 
 
-theorem StronglyMeromorphicOn_of_makeStronglyMeromorphic
-  {f : ℂ → ℂ}
-  (hf : MeromorphicOn f U) :
-  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+theorem stronglyMeromorphicOn_ratlPolynomial
+  {U : Set ℂ}
+  (d : ℂ → ℤ) :
+  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
+  by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite
+  · rw [finprod_eq_prod _ hd]
+    intro z h₁z
+    by_cases h₂z : d z = 0
+    · apply AnalyticAt.stronglyMeromorphicAt
+      rw [Finset.prod_fn]
+      apply Finset.analyticAt_prod
+      intro u hu
+      by_cases huz : u = z
+      · rw [← huz] at h₂z
+        rw [h₂z]
+        simp
+        exact analyticAt_const
+      · apply AnalyticAt.zpow
+        apply AnalyticAt.sub
+        apply analyticAt_id
+        apply analyticAt_const
+        rwa [sub_ne_zero, ne_comm]
+    · have : z ∈ hd.toFinset := by
+        simp
+        by_contra hCon
+        have A : 0 ≠ (1 : ℂ → ℂ) z := by simp
+        rw [← hCon] at A
+        simp only [sub_self] at A
+        rw [ne_comm] at A
+        rw [zpow_ne_zero_iff] at A
+        tauto
+        exact h₂z
+      rw [← Finset.mul_prod_erase hd.toFinset _ this]
+      right
+      use d z
+      use ∏ x ∈ hd.toFinset.erase z, fun z => (z - x) ^ d x
+      constructor
+      · rw [Finset.prod_fn]
+        apply Finset.analyticAt_prod
+        intro u hu
+        apply AnalyticAt.zpow
+        apply AnalyticAt.sub
+        apply analyticAt_id
+        apply analyticAt_const
+        rw [sub_ne_zero, ne_comm]
+        by_contra hCon
+        simp at hu
+        tauto
+      · constructor
+        · simp only [Finset.prod_apply]
+          rw [Finset.prod_ne_zero_iff]
+          intro u hu
+          rw [zpow_ne_zero_iff]
+          rw [sub_ne_zero]
+          by_contra hCon
+          rw [hCon] at hu
+          let A := Finset.not_mem_erase u hd.toFinset
+          tauto
+          --
+          have : u ∈ hd.toFinset := by
+            exact Finset.mem_of_mem_erase hu
+          simp at this
+          by_contra hCon
+          rw [hCon] at this
+          simp at this
+          tauto
+        · exact Filter.Eventually.of_forall (congrFun rfl)
 
-  sorry
+  · rw [finprod_of_infinite_mulSupport hd]
+    apply AnalyticOn.stronglyMeromorphicOn
+    apply analyticOnNhd_const
 
 
 theorem makeStronglyMeromorphicOn_changeDiscrete'