Nevanlinna/meromorphicOn_decompose.lean

@@ -10,17 +10,6 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
-theorem MeromorphicOn.order_ne_top
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsConnected U)
-  (h₂U : IsCompact U)
-  (h₁f : MeromorphicOn f U)
-  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
-  ∀ hz : z ∈ U, (h₁f z hz).order ≠ ⊤ := by
-
-  sorry
-
 
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}

Nevanlinna/stronglyMeromorphicAt.lean

@@ -348,7 +348,7 @@ theorem makeStronglyMeromorphic_id
   · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
 
 
-theorem StronglyMeromorphicAt.eliminate
+theorem StronglyMeromorphicAt.decompose
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (h₁f : StronglyMeromorphicAt f z₀)
@@ -357,6 +357,8 @@ theorem StronglyMeromorphicAt.eliminate
     ∧ (g z₀ ≠ 0)
     ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
 
+  let n := - h₁f.meromorphicAt.order.untop h₂f
+
   let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
   let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
   have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by