nevanlinna/Nevanlinna/holomorphic_zero.lean

import Init.Classical
import Mathlib.Analysis.Analytic.Meromorphic
import Mathlib.Topology.ContinuousOn
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.holomorphic
import Nevanlinna.analyticOn_zeroSet


noncomputable def zeroDivisor
  (f : ℂ → ℂ) :
  ℂ → ℕ := by
  intro z
  by_cases hf : AnalyticAt ℂ f z
  · exact hf.order.toNat
  · 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]


theorem zeroDivisor_eq_ord_AtZeroDivisorSupport'
  {f : ℂ → ℂ}
  {z : ℂ}
  (h : z ∈ Function.support (zeroDivisor f)) :
  zeroDivisor f z = (analyticAtZeroDivisorSupport h).order := by

  unfold zeroDivisor
  simp [analyticAtZeroDivisorSupport h]
  sorry


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_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 zeroDivisor_support_iff
  {f : ℂ → ℂ}
  {z₀ : ℂ} :
  z₀ ∈ Function.support (zeroDivisor f) ↔
  f z₀ = 0 ∧
  AnalyticAt ℂ f z₀ ∧
  ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by
  constructor
  · intro hz
    constructor
    · exact zeroDivisor_zeroSet hz
    · constructor
      · exact analyticAtZeroDivisorSupport hz
      · exact zeroDivisor_localDescription hz
  · intro ⟨h₁, h₂, h₃⟩
    have : zeroDivisor f z₀ = (h₂.order).toNat := by
      unfold zeroDivisor
      simp [h₂]
    simp [this]
    simp [(h₂.order_eq_nat_iff (zeroDivisor f z₀)).2 h₃]
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₃
    rw [Filter.Eventually.self_of_nhds h₃g] at h₁
    simp [h₂g] at h₁
    assumption


theorem topOnPreconnected
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) :
  ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by

  by_contra H
  push_neg at H
  obtain ⟨z', hz'⟩ := H
  rw [AnalyticAt.order_eq_top_iff] at hz'
  rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
  have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
  tauto


theorem supportZeroSet
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) :
  U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by

  ext x
  constructor
  · intro hx
    constructor
    · exact hx.1
    exact zeroDivisor_zeroSet hx.2
  · simp
    intro h₁x h₂x
    constructor
    · exact h₁x
    · let A := zeroDivisor_support_iff (f := f) (z₀ := x)
      simp at A
      rw [A]
      constructor
      · exact h₂x
      · constructor
        · exact h₁f x h₁x
        · have B := AnalyticAt.order_eq_nat_iff (h₁f x h₁x) (zeroDivisor f x)
          simp at B
          rw [← B]
          dsimp [zeroDivisor]
          simp [h₁f x h₁x]
          refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
          exact topOnPreconnected hU h₁f h₂f h₁x


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_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 : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed!
  (h₂U : IsCompact U) :
  Set.Finite (U ∩ Function.support (zeroDivisor f)) := by

  have hinter : IsCompact (U ∩ Function.support (zeroDivisor f)) := by
    apply IsCompact.of_isClosed_subset h₂U
    rw [supportZeroSet]
    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
    exact IsCompact.isClosed h₂U
    exact isClosed_singleton
    assumption
    assumption
    assumption
    exact Set.inter_subset_left

  apply hinter.finite
  apply DiscreteTopology.of_subset (s := Function.support (zeroDivisor f))
  exact discreteZeros (f := f)
  exact Set.inter_subset_right


theorem AnalyticOn.order_eq_nat_iff
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (hf : AnalyticOn ℂ f U)
  (hz₀ : z₀ ∈ U)
  (n : ℕ) :
  (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by

  constructor
  -- Direction →
  intro hn
  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn

  -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
  -- removable singularity removed
  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n

  -- Describe g near z₀
  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
    rw [eventually_nhds_iff]
    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
    use t
    constructor
    · intro y h₁y
      by_cases h₂y : y = z₀
      · dsimp [g]; simp [h₂y]
      · dsimp [g]; simp [h₂y]
        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
        exact h₁t y h₁y
        norm_num
        rw [sub_eq_zero]
        tauto
    · constructor
      · assumption
      · assumption

  -- Describe g near points z₁ that are different from z₀
  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
    intro hz₁
    rw [eventually_nhds_iff]
    use {z₀}ᶜ
    constructor
    · intro y hy
      simp at hy
      simp [g, hy]
    · exact ⟨isOpen_compl_singleton, hz₁⟩

  -- Use g and show that it has all required properties
  use g
  constructor
  · -- AnalyticOn ℂ g U
    intro z h₁z
    by_cases h₂z : z = z₀
    · rw [h₂z]
      apply AnalyticAt.congr h₁gloc
      exact Filter.EventuallyEq.symm g_near_z₀
    · simp_rw [eq_comm] at g_near_z₁
      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
      apply AnalyticAt.div
      exact hf z h₁z
      apply AnalyticAt.pow
      apply AnalyticAt.sub
      apply analyticAt_id
      apply analyticAt_const
      simp
      rw [sub_eq_zero]
      tauto
  · constructor
    · simp [g]; tauto
    · intro z
      by_cases h₂z : z = z₀
      · rw [h₂z, g_near_z₀.self_of_nhds]
        exact h₃gloc.self_of_nhds
      · rw [(g_near_z₁ h₂z).self_of_nhds]
        simp [h₂z]
        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
        simp; norm_num
        rw [sub_eq_zero]
        tauto

  -- direction ←
  intro h
  obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
  rw [AnalyticAt.order_eq_nat_iff]
  use g
  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩


theorem AnalyticOn.order_eq_nat_iff'
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {A : Finset U}
  (hf : AnalyticOn ℂ f U)
  (n : A → ℕ) :
  ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ a, (z - a) ^ (n a)) • g z := by

  apply Finset.induction

  let a : A := by sorry
  let b : ℂ := by sorry
  let u : U := by sorry

  let X := n a
  have : a = (3 : ℂ) := by sorry
  have : b ∈ ↑A := by sorry
  have : ↑a ∈ U := by exact Subtype.coe_prop a.val

  let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a

  --∀ a : A, (hf (ha a)).order = ↑(n a) →

  intro hn
  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn

  -- Define a candidate function
  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n

  -- Describe g near z₀
  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
    rw [eventually_nhds_iff]
    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
    use t
    constructor
    · intro y h₁y
      by_cases h₂y : y = z₀
      · dsimp [g]; simp [h₂y]
      · dsimp [g]; simp [h₂y]
        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
        exact h₁t y h₁y
        norm_num
        rw [sub_eq_zero]
        tauto
    · constructor
      · assumption
      · assumption

  -- Describe g near points z₁ different from z₀
  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
    intro hz₁
    rw [eventually_nhds_iff]
    use {z₀}ᶜ
    constructor
    · intro y hy
      simp at hy
      simp [g, hy]
    · exact ⟨isOpen_compl_singleton, hz₁⟩

  -- Use g and show that it has all required properties
  use g
  constructor
  · -- AnalyticOn ℂ g U
    intro z h₁z
    by_cases h₂z : z = z₀
    · rw [h₂z]
      apply AnalyticAt.congr h₁gloc
      exact Filter.EventuallyEq.symm g_near_z₀
    · simp_rw [eq_comm] at g_near_z₁
      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
      apply AnalyticAt.div
      exact hf z h₁z
      apply AnalyticAt.pow
      apply AnalyticAt.sub
      apply analyticAt_id
      apply analyticAt_const
      simp
      rw [sub_eq_zero]
      tauto
  · constructor
    · simp [g]; tauto
    · intro z
      by_cases h₂z : z = z₀
      · rw [h₂z, g_near_z₀.self_of_nhds]
        exact h₃gloc.self_of_nhds
      · rw [(g_near_z₁ h₂z).self_of_nhds]
        simp [h₂z]
        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
        simp; norm_num
        rw [sub_eq_zero]
        tauto


noncomputable def zeroDivisorDegree
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsPreconnected U) -- not needed!
  (h₂U : IsCompact U)
  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
  ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card


lemma zeroDivisorDegreeZero
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsPreconnected U) -- not needed!
  (h₂U : IsCompact U)
  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
  0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
  sorry


lemma eliminatingZeros₀
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U) :
  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
  (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
  ∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by

  intro n
  induction' n with n ih
  -- case zero
  intro f h₁f h₂f h₃f
  use f
  rw [zeroDivisorDegreeZero] at h₃f
  rw [h₃f]
  simpa

  -- case succ
  intro f h₁f h₂f h₃f

  let Supp := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset

  have : Supp.Nonempty := by
    rw [← Finset.one_le_card]
    calc 1
    _ ≤ n + 1 := by exact Nat.le_add_left 1 n
    _ = zeroDivisorDegree h₁U h₂U h₁f h₂f := by exact h₃f
    _ = Supp.card := by rfl
  obtain ⟨z₀, hz₀⟩ := this
  dsimp [Supp] at hz₀
  simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff] at hz₀




  let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
  rw [eq_comm] at B
  let C := A B
  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := C

  have h₄g₀ : ∃ z ∈ U, g₀ z ≠ 0 := by sorry
  have h₅g₀ : n = zeroDivisorDegree h₁U h₂U h₁g₀ h₄g₀ := by sorry

  obtain ⟨F, h₁F, h₂F⟩ := ih g₀ h₁g₀ h₄g₀ h₅g₀
  use F
  constructor
  · assumption
  ·
    sorry