Update holomorphic_zero.lean

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,122 @@ 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_localDescription
+  {f : ℂ → ℂ}
+  {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
+
+
 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_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
@@ -105,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
+
+  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