Implementing...

Nevanlinna/mathlibAddOn.lean

@@ -72,3 +72,20 @@ lemma Mnhds
     · simp at h₂y
       rwa [h₂y]
   · exact h₂t
+
+-- unclear where this should go
+
+lemma WithTopCoe
+  {n : WithTop ℕ} :
+  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
+  rcases n with h|h
+  · intro h
+    contradiction
+  · intro h₁
+    simp only [WithTop.map, Option.map] at h₁
+    have : (h : ℤ) = 0 := by
+      exact WithTop.coe_eq_zero.mp h₁
+    have : h = 0 := by
+      exact Int.ofNat_eq_zero.mp this
+    rw [this]
+    rfl

Nevanlinna/meromorphicOn_decompose.lean

@@ -4,26 +4,12 @@ import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
 import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.mathlibAddOn
 
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
-lemma WithTopCoe
-  {n : WithTop ℕ} :
-  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
-  rcases n with h|h
-  · intro h
-    contradiction
-  · intro h₁
-    simp only [WithTop.map, Option.map] at h₁
-    have : (h : ℤ) = 0 := by
-      exact WithTop.coe_eq_zero.mp h₁
-    have : h = 0 := by
-      exact Int.ofNat_eq_zero.mp this
-    rw [this]
-    rfl
-
 
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}

Nevanlinna/stronglyMeromorphicAt.lean

@@ -129,7 +129,45 @@ theorem StronglyMeromorphicAt.order_eq_zero_iff
   {z₀ : ℂ}
   (hf : StronglyMeromorphicAt f z₀) :
   hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by
-  sorry
+  constructor
+  · intro h₁f
+    let A := hf.analytic (le_of_eq (id (Eq.symm h₁f)))
+    apply A.order_eq_zero_iff.1
+    let B := A.meromorphicAt_order
+    rw [h₁f] at B
+    apply WithTopCoe
+    rw [eq_comm]
+    exact B
+  · intro h
+    have hf' := hf
+    rcases hf with h₁|h₁
+    · have : f z₀ = 0 := by
+        apply Filter.EventuallyEq.eq_of_nhds h₁
+      tauto
+    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁
+      have : n = 0 := by
+        by_contra hContra
+        let A := Filter.EventuallyEq.eq_of_nhds h₃g
+        have : (0 : ℂ) ^ n = 0 := by
+          exact zero_zpow n hContra
+        simp at A
+        simp_rw [this] at A
+        simp at A
+        tauto
+      rw [this] at h₃g
+      simp at h₃g
+
+      have : hf'.meromorphicAt.order = 0 := by
+        apply (hf'.meromorphicAt.order_eq_int_iff 0).2
+        use g
+        constructor
+        · assumption
+        · constructor
+          · assumption
+          · simp
+            apply Filter.EventuallyEq.filter_mono h₃g
+            exact nhdsWithin_le_nhds
+      exact this
 
 theorem StronglyMeromorphicAt.localIdentity
   {f g : ℂ → ℂ}