From 9d4657fb81e85de8f737982919d55d41321d767a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 16 Aug 2024 15:20:24 +0200
Subject: [PATCH] Update holomorphic_zero.lean

---
 Nevanlinna/holomorphic_zero.lean | 61 +++++++++++++++++++++++++++-----
 1 file changed, 53 insertions(+), 8 deletions(-)

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 7d8b1a3..d03bb2d 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -50,13 +50,43 @@ lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : ℕ, m = n
   contrapose; simp; tauto
 
 
-theorem zeroDivisor_in_zeroSet
+theorem zeroDivisor_localDescription
   {f : ℂ → ℂ}
-  {z : ℂ}
-  (h : z ∈ Function.support (zeroDivisor f)) :
-  f z = 0 := by
+  {z₀ : ℂ}
+  (h : z₀ ∈ Function.support (zeroDivisor f)) :
+  ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by
+
+  have A : zeroDivisor f ↑z₀ ≠ 0 := by exact h
+  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport h
+  rw [B] at A
+  have C := natural_if_toNatNeZero A
+  obtain ⟨m, hm⟩ := C
+  have h₂m : m ≠ 0 := by
+    rw [← hm] at A
+    simp at A
+    assumption
+  rw [eq_comm] at hm
+  let E := AnalyticAt.order_eq_nat_iff (analyticAtZeroDivisorSupport h) m
+  let F := hm
+  rw [E] at F
+
+  have : m = zeroDivisor f z₀ := by
+    rw [B, hm]
+    simp
+  rwa [this] at F
+
+
+theorem zeroDivisor_zeroSet
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h : z₀ ∈ Function.support (zeroDivisor f)) :
+  f z₀ = 0 := by
+  obtain ⟨g, _, _, h₃⟩ := zeroDivisor_localDescription h
+  rw [Filter.Eventually.self_of_nhds h₃]
+  simp
+  left
+  exact h
 
-  sorry
 
 theorem discreteZeros
   {f : ℂ → ℂ} :
@@ -121,7 +151,7 @@ theorem discreteZeros
     _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
   let F := h₂ε₂ y.1 h₂y
-  rw [zeroDivisor_in_zeroSet y.2] at F
+  rw [zeroDivisor_zeroSet y.2] at F
   simp at F
 
   simp [h₂m] at F
@@ -145,7 +175,22 @@ theorem eliminatingZeros
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   {R : ℝ}
-  (h₁f : ∀ z ∈ Metric.ball z₀ R, HolomorphicAt f z)
+  (h₁f : ∀ z ∈ Metric.closedBall z₀ R, HolomorphicAt f z)
   (h₂f : ∃ z ∈ Metric.ball z₀ R, f z ≠ 0) :
   ∃ F : ℂ → ℂ, ∀ z ∈ Metric.ball z₀ R, (HolomorphicAt F z) ∧ (f z = (F z) * ∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a) ) := by
-  sorry
+
+  let F : ℂ → ℂ := by
+    intro z
+    if hz : z ∈ (Metric.closedBall z₀ R) ∩ Function.support (zeroDivisor f) then
+      exact 0
+    else
+      exact f z * (∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a))⁻¹
+
+  use F
+  intro z hz
+  by_cases h₂z : z ∈ (Metric.closedBall z₀ R) ∩ Function.support (zeroDivisor f)
+  · -- Positive case
+    sorry
+
+  · -- Negative case
+    sorry