Nevanlinna/holomorphic_zero.lean

@@ -23,15 +23,6 @@ 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₁
@@ -45,122 +36,61 @@ 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
-
-  simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
+  apply singletons_open_iff_discrete.mp
   intro z
 
-  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
+  let A := analyticAtZeroDivisorSupport z.2
+  let c : WithTop ℕ := A.order
+  let B := AnalyticAt.order_eq_nat_iff A
+  let n := zeroDivisor f z.1
 
-  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
 
-    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
+  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
 
-  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
 
-  have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
-    simp
-    calc dist y z
-    _ < min ε₁ ε₂ := by assumption
-    _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
+    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_left ε₁ ε₂
 
-  let F := h₂ε₂ y.1 h₂y
-  rw [zeroDivisor_zeroSet y.2] at F
-  simp at F
 
-  simp [h₂m] at F
 
-  have : g y.1 ≠ 0 := by
-    exact h₁ε₁.2 y h₃y
-  simp [this] at F
-  ext
-  rwa [sub_eq_zero] 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
 
 
 theorem zeroDivisor_finiteOnCompact
@@ -175,22 +105,7 @@ theorem eliminatingZeros
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   {R : ℝ}
-  (h₁f : ∀ z ∈ Metric.closedBall z₀ R, HolomorphicAt f z)
+  (h₁f : ∀ z ∈ Metric.ball 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