Update holomorphic_zero.lean

Nevanlinna/holomorphic_zero.lean

@@ -6,10 +6,9 @@ noncomputable def zeroDivisor
   (f : ℂ → ℂ) :
   ℂ → ℕ := by
   intro z
-  if hf : AnalyticAt ℂ f z then
-    exact hf.order.toNat
-  else
-    exact 0
+  by_cases hf : AnalyticAt ℂ f z
+  · exact hf.order.toNat
+  · exact 0
 
 
 theorem analyticAtZeroDivisorSupport
@@ -17,6 +16,7 @@ theorem analyticAtZeroDivisorSupport
   {z : ℂ}
   (h : z ∈ Function.support (zeroDivisor f)) :
   AnalyticAt ℂ f z := by
+
   by_contra h₁f
   simp at h
   dsimp [zeroDivisor] at h
@@ -28,6 +28,7 @@ theorem zeroDivisor_eq_ord_AtZeroDivisorSupport
   {z : ℂ}
   (h : z ∈ Function.support (zeroDivisor f)) :
   zeroDivisor f z = (analyticAtZeroDivisorSupport h).order.toNat := by
+
   unfold zeroDivisor
   simp [analyticAtZeroDivisorSupport h]
 
@@ -88,6 +89,32 @@ theorem zeroDivisor_zeroSet
   exact h
 
 
+theorem zeroDivisor_support_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ} :
+  z₀ ∈ Function.support (zeroDivisor f) ↔
+  f z₀ = 0 ∧
+  AnalyticAt ℂ f z₀ ∧
+  ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by
+  constructor
+  · intro hz
+    constructor
+    · exact zeroDivisor_zeroSet hz
+    · constructor
+      · exact analyticAtZeroDivisorSupport hz
+      · exact zeroDivisor_localDescription hz
+  · intro ⟨h₁, h₂, h₃⟩
+    have : zeroDivisor f z₀ = (h₂.order).toNat := by
+      unfold zeroDivisor
+      simp [h₂]
+    simp [this]
+    simp [(h₂.order_eq_nat_iff (zeroDivisor f z₀)).2 h₃]
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₃
+    rw [Filter.Eventually.self_of_nhds h₃g] at h₁
+    simp [h₂g] at h₁
+    assumption
+
+
 theorem discreteZeros
   {f : ℂ → ℂ} :
   DiscreteTopology (Function.support (zeroDivisor f)) := by