Working…

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

Nevanlinna/stronglyMeromorphicOn.lean

@@ -27,7 +27,7 @@ theorem StronglyMeromorphicOn.analytic
   {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
+  AnalyticOnNhd ℂ f U := by
   intro z hz
   apply StronglyMeromorphicAt.analytic
   exact h₂f z hz

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -324,7 +324,6 @@ theorem MeromorphicOn.decompose₃
     · apply AnalyticAt.analyticWithinAt
       rw [analyticAt_of_mul_analytic]
 
-
       sorry
 
   have h₂h : StronglyMeromorphicOn h U := by
@@ -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