nevanlinna/Nevanlinna/holomorphic_zero.lean

import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.holomorphic


noncomputable def zeroDivisor
  (f : ℂ → ℂ) :
  ℂ → ℕ := by
  intro z
  if hf : AnalyticAt ℂ f z then
    exact hf.order.toNat
  else
    exact 0


theorem analyticAtZeroDivisorSupport
  {f : ℂ → ℂ}
  {z : ℂ}
  (h : z ∈ Function.support (zeroDivisor f)) :
  AnalyticAt ℂ f z := by
  by_contra h₁f
  simp at h
  dsimp [zeroDivisor] at h
  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₁
    rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists]
    by_contra H₂
    rw [H₂] at H₁
    simp at H₁
  · intro H
    obtain ⟨m, hm⟩ := H
    rw [← hm]
    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

  simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
  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

  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

  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 ε₁ ε₂

  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

  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
  {f : ℂ → ℂ}
  {s : Set ℂ}
  (hs : IsCompact s) :
  Set.Finite (s ∩ Function.support (zeroDivisor f)) := by
  sorry


theorem eliminatingZeros
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  {R : ℝ}
  (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
  sorry