nevanlinna/Nevanlinna/stronglyMeromorphic.lean

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


/- 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₃g⟩ := h
    have : MeromorphicAt (fun z ↦ (z - z₀) ^ n • g z) z₀ := by
      simp
      apply MeromorphicAt.mul
      apply MeromorphicAt.zpow
      apply MeromorphicAt.sub

      sorry
    apply MeromorphicAt.congr this
    rw [Filter.eventuallyEq_comm]
    exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds


/- Strongly MeromorphicAt of positive order is analytic -/
theorem StronglyMeromorphicAt.analytic
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁f : StronglyMeromorphicAt f z₀)
  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
  AnalyticAt ℂ f z₀ := by
  sorry



/- Make strongly MeromorphicAt -/

def MeromorphicAt.makeStronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ℂ → ℂ := by
  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