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

---
 Nevanlinna/holomorphic_zero.lean | 120 ++++++++++++++++++++-----------
 1 file changed, 80 insertions(+), 40 deletions(-)

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 8362bf5..7d8b1a3 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -23,6 +23,15 @@ theorem analyticAtZeroDivisorSupport
   simp [h₁f] at h
 
 
+theorem zeroDivisor_eq_ord_AtZeroDivisorSupport
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : z ∈ Function.support (zeroDivisor f)) :
+  zeroDivisor f z = (analyticAtZeroDivisorSupport h).order.toNat := by
+  unfold zeroDivisor
+  simp [analyticAtZeroDivisorSupport h]
+
+
 lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : ℕ, m = n := by
   constructor
   · intro H₁
@@ -36,61 +45,92 @@ lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : ℕ, m = n := by
     simp
 
 
+lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : ℕ, m = n := by
+  rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists]
+  contrapose; simp; tauto
+
+
+theorem zeroDivisor_in_zeroSet
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : z ∈ Function.support (zeroDivisor f)) :
+  f z = 0 := by
+
+  sorry
+
 theorem discreteZeros
   {f : ℂ → ℂ} :
   DiscreteTopology (Function.support (zeroDivisor f)) := by
-  apply singletons_open_iff_discrete.mp
+
+  simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
   intro z
 
-  let A := analyticAtZeroDivisorSupport z.2
-  let c : WithTop ℕ := A.order
-  let B := AnalyticAt.order_eq_nat_iff A
-  let n := zeroDivisor f z.1
+  have A : zeroDivisor f ↑z ≠ 0 := by exact z.2
+  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport z.2
+  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 z.2) m
+  rw [E] at hm
 
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := hm
 
+  rw [Metric.eventually_nhds_iff_ball] at h₃g
+  have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by
+    have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g
+    have : {0}ᶜ ∈ nhds (g z) := by
+      exact compl_singleton_mem_nhds_iff.mpr h₂g
 
-  have : ∃ a : ℕ, a = A.order := by
-    rw [← ENat.some_eq_coe]
-    rw [← WithTop.ne_top_iff_exists]
-    by_contra H
-    rw [AnalyticAt.order_eq_top_iff] at H
+    let F := h₄g.preimage_mem_nhds this
+    rw [Metric.mem_nhds_iff] at F
+    obtain ⟨ε, h₁ε, h₂ε⟩ := F
+    use ε
+    constructor; exact h₁ε
+    intro y hy
+    let G := h₂ε hy
+    simp at G
+    exact G
+  obtain ⟨ε₁, h₁ε₁⟩ := this
 
+  obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
+  use min ε₁ ε₂
+  constructor
+  · have : 0 < min ε₁ ε₂ := by
+      rw [lt_min_iff]
+      exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
+    exact this
 
+  intro y
+  intro h₁y
 
-    dsimp [n, zeroDivisor]
-    simp [A]
+  have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
+    simp
+    calc dist y z
+    _ < min ε₁ ε₂ := by assumption
+    _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
 
+  have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by
+    simp
+    calc dist y z
+    _ < min ε₁ ε₂ := by assumption
+    _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
+  let F := h₂ε₂ y.1 h₂y
+  rw [zeroDivisor_in_zeroSet y.2] at F
+  simp at F
 
+  simp [h₂m] at F
 
-
-    sorry
-  let C := (B n).1 this
-
-  apply Metric.isOpen_singleton_iff.mpr
-
-
-
-  /-
-
-Try this: refine Metric.isOpen_singleton_iff.mpr ?_
-Remaining subgoals:
-⊢ ∃ ε > 0, ∀ (y : ↑(Function.support (zeroDivisor f))), dist y z < ε → y = z
-Suggestions
-Try this: refine isClosed_compl_iff.mp ?_
-Remaining subgoals:
-⊢ IsClosed {z}ᶜ
-Suggestions
-Try this: refine disjoint_frontier_iff_isOpen.mp ?_
-Remaining subgoals:
-⊢ Disjoint (frontier {z}) {z}
-Suggestions
-Try this: refine isOpen_iff_forall_mem_open.mpr ?_
-Remaining subgoals:
-⊢ ∀ x ∈ {z}, ∃ t ⊆ {z}, IsOpen t ∧ x ∈ t
-
-  -/
-  sorry
+  have : g y.1 ≠ 0 := by
+    exact h₁ε₁.2 y h₃y
+  simp [this] at F
+  ext
+  rwa [sub_eq_zero] at F
 
 
 theorem zeroDivisor_finiteOnCompact