nevanlinna/Nevanlinna/stronglyMeromorphic.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.mathlibAddOn


/- Strongly MeromorphicAt -/
def StronglyMeromorphicAt
  (f : ℂ → ℂ)
  (z₀ : ℂ) :=
  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))


/- Strongly MeromorphicAt is Meromorphic -/
theorem StronglyMeromorphicAt.meromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : StronglyMeromorphicAt f z₀) :
  MeromorphicAt f z₀ := by
  rcases hf with h|h
  · use 0; simp
    rw [analyticAt_congr h]
    exact analyticAt_const
  · obtain ⟨n, g, h₁g, _, h₃g⟩ := h
    rw [meromorphicAt_congr' h₃g]
    apply MeromorphicAt.smul
    apply MeromorphicAt.zpow
    apply MeromorphicAt.sub
    apply MeromorphicAt.id
    apply MeromorphicAt.const
    exact AnalyticAt.meromorphicAt h₁g


/- Strongly MeromorphicAt of non-negative order is analytic -/
theorem StronglyMeromorphicAt.analytic
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁f : StronglyMeromorphicAt f z₀)
  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
  AnalyticAt ℂ f z₀ := by
  let h₁f' := h₁f
  rcases h₁f' with h|h
  · rw [analyticAt_congr h]
    exact analyticAt_const
  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
    rw [analyticAt_congr h₃g]

    have : h₁f.meromorphicAt.order = n := by
      rw [MeromorphicAt.order_eq_int_iff]
      use g
      constructor
      · exact h₁g
      · constructor
        · exact h₂g
        · exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
    rw [this] at h₂f
    apply AnalyticAt.smul
    nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
    apply AnalyticAt.pow
    apply AnalyticAt.sub
    apply analyticAt_id -- Warning: want apply AnalyticAt.id
    apply analyticAt_const -- Warning: want AnalyticAt.const
    exact h₁g


/- Analytic functions are strongly meromorphic -/
theorem AnalyticAt.stronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁f : AnalyticAt ℂ f z₀) :
  StronglyMeromorphicAt f z₀ := by
  by_cases h₂f : h₁f.order = ⊤
  · rw [AnalyticAt.order_eq_top_iff] at h₂f
    tauto
  · have : h₁f.order ≠ ⊤ := h₂f
    rw [← ENat.coe_toNat_eq_self] at this
    rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
    right
    use h₁f.order.toNat
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
    use g
    tauto


theorem MeromorphicAt.order_neq_top_iff
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ (hf.order.untop' 0) • g z := by

  rw [← hf.order_eq_int_iff (hf.order.untop' 0)]
  constructor
  · intro h₁f
    apply?
    exact Eq.symm (ENat.coe_toNat h₁f)
  · intro h₁f
    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))


/- Make strongly MeromorphicAt -/
noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ℂ → ℂ := by

  by_cases h₁f : hf.order = ⊤
  · exact 0
  ·

  intro z
  by_cases z = z₀
  · by_cases h₂f : hf.order = 0
    · have : (0 : WithTop ℤ) = (0 : ℤ) := rfl
      rw [this, hf.order_eq_int_iff] at h₂f
      exact (Classical.choose h₂f) z₀
    · exact 0
  · exact f z


theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by



  by_cases h₂f : hf.order = 0
  · apply AnalyticAt.stronglyMeromorphicAt

    let A := h₂f
    rw [(by rfl : (0 : WithTop ℤ) = (0 : ℤ)), hf.order_eq_int_iff] at A
    simp at A
    have : hf.makeStronglyMeromorphicAt = Classical.choose A := by
      simp [MeromorphicAt.makeStronglyMeromorphicAt, h₂f]
    let B := Classical.choose_spec A

    rw [this]
    tauto
  · by_cases h₃f : hf.order = ⊤
    · rw [MeromorphicAt.order_eq_top_iff] at h₃f
      left

      sorry
    · sorry



theorem makeStronglyMeromorphic_eventuallyEq
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
  sorry