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


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


theorem discreteZeros
  {f : ℂ → ℂ} :
  DiscreteTopology (Function.support (zeroDivisor f)) := by
  apply singletons_open_iff_discrete.mp
  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 : ℕ, 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



    dsimp [n, zeroDivisor]
    simp [A]





    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
  {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