working

Nevanlinna/meromorphicOn_decompose.lean

@@ -0,0 +1,23 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn_divisor
+import Nevanlinna.stronglyMeromorphicOn
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+theorem MeromorphicOn.decompose
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsConnected U)
+  (h₂U : IsCompact U)
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
+  ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
+    ∧ (∀ z ∈ U, g z ≠ 0)
+    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p ∈ h₁f.divisor.support, (z-p) ) U) := by
+  sorry

Nevanlinna/stronglyMeromorphicAt.lean

@@ -155,7 +155,7 @@ lemma m₂
   apply eventually_nhdsWithin_of_forall
   exact fun x a => m₁ hf x a
 
-
+/-
 lemma Mnhds
   {f g : ℂ → ℂ}
   {z₀ : ℂ}
@@ -172,7 +172,7 @@ lemma Mnhds
     · simp at h₂y
       rwa [h₂y]
   · exact h₂t
-
+-/
 
 theorem localIdentity
   {f g : ℂ → ℂ}
@@ -262,7 +262,7 @@ theorem makeStronglyMeromorphic_id
   · rw [hz]
     unfold MeromorphicAt.makeStronglyMeromorphicAt
     simp
-    let h₀f := hf
+    have h₀f := hf
     rcases hf with h₁f|h₁f
     · have A : f =ᶠ[𝓝[≠] z₀] 0 := by
         apply Filter.EventuallyEq.filter_mono h₁f