working...

Nevanlinna/meromorphicOn_decompose.lean

@@ -63,5 +63,7 @@ theorem MeromorphicOn.decompose
         sorry
       have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
         sorry
+      apply Filter.EventuallyEq.eq_of_nhds
+      apply StronglyMeromorphicAt.localIdentity
 
       sorry

Nevanlinna/stronglyMeromorphicAt.lean

@@ -169,6 +169,7 @@ theorem StronglyMeromorphicAt.order_eq_zero_iff
             exact nhdsWithin_le_nhds
       exact this
 
+
 theorem StronglyMeromorphicAt.localIdentity
   {f g : ℂ → ℂ}
   {z₀ : ℂ}

Nevanlinna/stronglyMeromorphicOn.lean

@@ -45,32 +45,6 @@ theorem AnalyticOn.stronglyMeromorphicOn
   exact h₁f z hz
 
 
-/- Strongly meromorphic functions on compact, preconnected sets are quotients of analytic functions -/
-theorem StronglyMeromorphicOn_finite
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsCompact U)
-  (h₂U : IsPreconnected U)
-  (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ z ∈ U, f z ≠ 0) :
-  Set.Finite {z ∈ U | f z = 0} := by
-
-  sorry
-
-
-/- Strongly meromorphic functions on compact, preconnected sets are quotients of analytic functions -/
-theorem StronglyMeromorphicOn_quotient
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsCompact U)
-  (h₂U : IsPreconnected U)
-  (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ z ∈ U, f z ≠ 0) :
-  ∃ a b : ℂ → ℂ, (AnalyticOnNhd ℂ a U) ∧ (AnalyticOnNhd ℂ b U) ∧ (∀ z ∈ U, a z ≠ 0 ∨ b z ≠ 0) ∧ f = a / b := by
-
-  sorry
-
-
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
@@ -105,6 +79,14 @@ theorem makeStronglyMeromorphicOn_changeDiscrete
     · simp [h₂v]
 
 
+theorem StronglyMeromorphicOn_of_makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+  sorry
+
+
 theorem makeStronglyMeromorphicOn_changeDiscrete'
   {f : ℂ → ℂ}
   {U : Set ℂ}