working…

Nevanlinna/meromorphicOn_divisor.lean

@@ -2,6 +2,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
+import Nevanlinna.stronglyMeromorphicOn
 
 
 open scoped Interval Topology
@@ -142,3 +143,19 @@ theorem MeromorphicOn.divisor_mul
     rw [Function.nmem_support.mp (fun a => hz (h₁f₂.divisor.supportInU a))]
     rw [Function.nmem_support.mp (fun a => hz ((h₁f₁.mul h₁f₂).divisor.supportInU a))]
     simp
+
+
+theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  hf.divisor = (stronglyMeromorphicOn_of_makeStronglyMeromorphicOn hf).meromorphicOn.divisor := by
+  unfold MeromorphicOn.divisor
+  simp
+  funext z
+  by_cases hz : z ∈ U
+  · simp [hz]
+    congr 1
+    apply MeromorphicAt.order_congr
+    exact EventuallyEq.symm (makeStronglyMeromorphicOn_changeDiscrete hf hz)
+  · simp [hz]

Nevanlinna/stronglyMeromorphicOn.lean

@@ -1,4 +1,3 @@
-import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicAt
 import Mathlib.Algebra.BigOperators.Finprod
 
@@ -46,7 +45,7 @@ theorem AnalyticOn.stronglyMeromorphicOn
   exact h₁f z hz
 
 
-/- Make strongly MeromorphicAt -/
+/- Make strongly MeromorphicOn -/
 noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}
@@ -78,3 +77,28 @@ theorem makeStronglyMeromorphicOn_changeDiscrete
       rw [← StronglyMeromorphicAt.makeStronglyMeromorphic_id]
       exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
     · simp [h₂v]
+
+
+theorem makeStronglyMeromorphicOn_changeDiscrete'
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
+  apply Mnhds
+  · apply Filter.EventuallyEq.trans (makeStronglyMeromorphicOn_changeDiscrete hf hz₀)
+    exact m₂ (hf z₀ hz₀)
+  · rw [MeromorphicOn.makeStronglyMeromorphicOn]
+    simp [hz₀]
+
+
+theorem stronglyMeromorphicOn_of_makeStronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+  intro z hz
+  let A := makeStronglyMeromorphicOn_changeDiscrete' hf hz
+  rw [stronglyMeromorphicAt_congr A]
+  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z hz)

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -5,6 +5,7 @@ import Nevanlinna.meromorphicAt
 import Nevanlinna.meromorphicOn
 import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.stronglyMeromorphicOn_ratlPolynomial
 import Nevanlinna.mathlibAddOn
 
 open scoped Interval Topology
@@ -314,12 +315,20 @@ theorem MeromorphicOn.decompose₃
     apply h₃f
 
   obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP
-
   let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1
+  have h₅g : AnalyticOn ℂ g U := by
+    intro z hz
+    by_cases h₂z : ⟨z, hz⟩ ∈ P
+    · apply AnalyticAt.analyticWithinAt
+      exact h₂g ⟨⟨z, hz⟩, h₂z⟩
+    · apply AnalyticAt.analyticWithinAt
+      rw [analyticAt_of_mul_analytic]
+
+
+    sorry
 
   have h₂h : StronglyMeromorphicOn h U := by
-    unfold h
-    apply stronglyMeromorphicOn_ratlPolynomial₂
+    sorry
   have h₁h : MeromorphicOn h U := by
     exact StronglyMeromorphicOn.meromorphicOn h₂h
   have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by
@@ -339,3 +348,61 @@ theorem MeromorphicOn.decompose₃
         congr
         simp
         sorry
+
+
+
+theorem MeromorphicOn.decompose₃'
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsCompact U)
+  (h₂U : IsConnected U)
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∃ u : U, f u ≠ 0) :
+  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
+    ∧ (AnalyticOn ℂ g U)
+    ∧ (∀ u : U, g u ≠ 0)
+    ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by
+
+  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f
+  have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
+
+  let d := - h₁f.meromorphicOn.divisor.toFun
+  let h₁ := ∏ᶠ u, fun z ↦ (z - u) ^ (d u)
+  have h₁h₁ : StronglyMeromorphicOn h₁ U := by
+    intro z hz
+    exact stronglyMeromorphicOn_ratlPolynomial₃ d z trivial
+  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
+    rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn _]
+    unfold MeromorphicOn.divisor
+    simp
+    funext z
+    by_cases hz : z ∈ U
+    · simp [hz]
+      have : (Function.support d).Finite := by
+        sorry
+      rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d this]
+      simp
+      sorry
+    · simp [hz]
+    sorry
+
+  let g := h₁g'.makeStronglyMeromorphicOn
+  have h₁g : StronglyMeromorphicOn g U := by
+    sorry
+  have h₂g : h₁g.meromorphicOn.divisor.toFun = 0 := by
+    sorry
+  have h₃g : AnalyticOn ℂ g U := by
+    sorry
+  have h₄g : ∀ u : U, g u ≠ 0 := by
+    sorry
+
+  use g
+  constructor
+  · exact StronglyMeromorphicOn.meromorphicOn h₁g
+  · constructor
+    · exact h₃g
+    · constructor
+      · exact h₄g
+      · sorry

Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean

@@ -1,4 +1,5 @@
 import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.mathlibAddOn
 
 open scoped Interval Topology
@@ -141,28 +142,3 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial
   simp
   rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d h₁d]
   simp
-
-
-theorem makeStronglyMeromorphicOn_changeDiscrete'
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicOn f U)
-  (hz₀ : z₀ ∈ U) :
-  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
-  apply Mnhds
-  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
-  apply Filter.EventuallyEq.trans A
-  exact m₂ (hf z₀ hz₀)
-  unfold MeromorphicOn.makeStronglyMeromorphicOn
-  simp [hz₀]
-
-
-theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : MeromorphicOn f U) :
-  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-  intro z₀ hz₀
-  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
-  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)