nevanlinna/Nevanlinna/analyticOn_zeroSet.lean

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



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, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by

  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)

  -- case empty
  simp
  use f
  simp
  exact hf

  -- case insert
  intro b₀ B hb iHyp
  intro hBinsert
  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))

  have : (h₁g₀ b₀ b₀.2).order = n b₀ := by sorry
  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this

  use g₁
  constructor
  · exact h₁g₁
  · constructor
    · intro a h₁a
      by_cases h₂a : a = b₀
      · rwa [h₂a]
      · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
        let B' := h₃g₁ a
        let C' := h₂g₀ a A'
        rw [B'] at C'
        exact right_ne_zero_of_smul C'
    · intro z
      let A' := h₃g₀ z
      rw [h₃g₁ z] at A'
      rw [A']
      rw [← smul_assoc]
      congr
      simp
      rw [Finset.prod_insert]
      ring
      exact hb