working

Nevanlinna/meromorphicOn_decompose.lean

@@ -10,6 +10,17 @@ 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.decompose
+theorem StronglyMeromorphicAt.eliminate
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (h₁f : StronglyMeromorphicAt f z₀)
@@ -357,8 +357,6 @@ theorem StronglyMeromorphicAt.decompose
     ∧ (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