Nevanlinna/meromorphicOn_divisor.lean

@@ -159,26 +159,3 @@ 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

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) :
-  AnalyticOnNhd ℂ f U := by
+  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
+  ∀ z ∈ U, AnalyticAt ℂ f z := by
   intro z hz
   apply StronglyMeromorphicAt.analytic
   exact h₂f z hz

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -324,7 +324,8 @@ theorem MeromorphicOn.decompose₃
     · apply AnalyticAt.analyticWithinAt
       rw [analyticAt_of_mul_analytic]
 
-      sorry
+
+    sorry
 
   have h₂h : StronglyMeromorphicOn h U := by
     sorry
@@ -382,8 +383,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
@@ -393,26 +394,20 @@ theorem MeromorphicOn.decompose₃'
     simp
 
   let g := h₁g'.makeStronglyMeromorphicOn
-  have h₁g : StronglyMeromorphicOn g U := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁g'
+  have h₁g : StronglyMeromorphicOn g U := by
+    sorry
   have h₂g : h₁g.meromorphicOn.divisor.toFun = 0 := by
-    rw [← MeromorphicOn.divisor_of_makeStronglyMeromorphicOn]
-    rw [h₂g']
-  have h₃g : AnalyticOnNhd ℂ g U := by
-    apply StronglyMeromorphicOn.analyticOnNhd
-    rw [h₂g]
-    simp
-    assumption
+    sorry
+  have h₃g : AnalyticOn ℂ g U := by
+    sorry
   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 AnalyticOnNhd.analyticOn h₃g
+    · exact h₃g
     · constructor
       · exact h₄g
       · sorry

Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean

@@ -63,13 +63,6 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃
     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₁
   {z : ℂ}
@@ -173,10 +166,7 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃order
     have : (Function.mulSupport fun u z => (z - u) ^ d u).Infinite := by
       exact hd
     simp_rw [finprod_of_infinite_mulSupport this]
-    have : AnalyticAt ℂ (1 : ℂ → ℂ) z := by exact analyticAt_const
-    rw [AnalyticAt.meromorphicAt_order this]
-    rw [this.order_eq_zero_iff.2 (by simp)]
-    simp
+    sorry
 
 
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial