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


/- Make strongly MeromorphicAt -/
noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ℂ → ℂ := by
  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
  · exact 0


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

  sorry


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