nevanlinna/Nevanlinna/stronglyMeromorphicAt.lean

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


open Topology


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


/- Strong meromorphic depends only on germ -/
theorem stronglyMeromorphicAt_congr
  {f g : ℂ → ℂ}
  {z₀ : ℂ}
  (hfg : f =ᶠ[𝓝 z₀] g) :
  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt g z₀ := by
  unfold StronglyMeromorphicAt
  constructor
  · intro h
    rcases h with h|h
    · left
      exact Filter.EventuallyEq.rw h (fun x => Eq (g x)) (id (Filter.EventuallyEq.symm hfg))
    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
      right
      use n
      use h
      constructor
      · assumption
      · constructor
        · assumption
        · apply Filter.EventuallyEq.trans hfg.symm
          assumption
  · intro h
    rcases h with h|h
    · left
      exact Filter.EventuallyEq.rw h (fun x => Eq (f x)) hfg
    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
      right
      use n
      use h
      constructor
      · assumption
      · constructor
        · assumption
        · apply Filter.EventuallyEq.trans hfg
          assumption


/- Make strongly MeromorphicAt -/
noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ℂ → ℂ := by
  intro z
  by_cases z = z₀
  · by_cases h₁f : hf.order = (0 : ℤ)
    · rw [hf.order_eq_int_iff] at h₁f
      exact (Classical.choose h₁f) z₀
    · exact 0
  · exact f z


lemma m₁
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
  intro z hz
  unfold MeromorphicAt.makeStronglyMeromorphicAt
  simp [hz]


lemma m₂
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
  apply eventually_nhdsWithin_of_forall
  exact fun x a => m₁ hf x a


lemma Mnhds
  {f g : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
  (h₂ : f z₀ = g z₀) :
  f =ᶠ[𝓝 z₀] g := by
  apply eventually_nhds_iff.2
  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
  use t
  constructor
  · intro y hy
    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
    · exact h₁t y hy h₂y
    · simp at h₂y
      rwa [h₂y]
  · exact h₂t


theorem localIdentity
  {f g : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : AnalyticAt ℂ f z₀)
  (hg : AnalyticAt ℂ g z₀) :
  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
  intro h
  let Δ := f - g
  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
    exact Filter.eventuallyEq_iff_sub.mp h

  have : Δ =ᶠ[𝓝 z₀] 0 := by
    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
    · exact h
    · have := Filter.EventuallyEq.eventually t₁
      let A := Filter.eventually_and.2 ⟨this, h⟩
      let _ := Filter.Eventually.exists A
      tauto
  exact Filter.eventuallyEq_iff_sub.mpr this


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

  by_cases h₂f : hf.order = ⊤
  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
      apply Mnhds
      · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
        exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
      · unfold MeromorphicAt.makeStronglyMeromorphicAt
        simp [h₂f]

    apply AnalyticAt.stronglyMeromorphicAt
    rw [analyticAt_congr this]
    apply analyticAt_const
  · let n := hf.order.untop h₂f
    have : hf.order = n := by
      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
    rw [hf.order_eq_int_iff] at this
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
    right
    use n
    use g
    constructor
    · assumption
    · constructor
      · assumption
      · apply Mnhds
        · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
          exact h₃g
        · unfold MeromorphicAt.makeStronglyMeromorphicAt
          simp
          by_cases h₃f : hf.order = (0 : ℤ)
          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
            simp [h₃f]
            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
            simp at h₃G
            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
            rw [hn]
            rw [hn] at h₃g; simp at h₃g
            simp
            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
              apply localIdentity h₁g h₁G
              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
            rw [Filter.EventuallyEq.eq_of_nhds this]
          · have : hf.order ≠ 0 := h₃f
            simp [this]
            left
            apply zero_zpow n
            dsimp [n]
            rwa [WithTop.untop_eq_iff h₂f]


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

  funext z
  by_cases hz : z = z₀
  · rw [hz]
    unfold MeromorphicAt.makeStronglyMeromorphicAt
    simp
    let h₀f := hf
    rcases hf with h₁f|h₁f
    · have A : f =ᶠ[𝓝[≠] z₀] 0 := by
        apply Filter.EventuallyEq.filter_mono h₁f
        exact nhdsWithin_le_nhds
      let B := (MeromorphicAt.order_eq_top_iff h₀f.meromorphicAt).2 A
      simp [B]
      exact Filter.EventuallyEq.eq_of_nhds h₁f
    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
      rw [Filter.EventuallyEq.eq_of_nhds h₃g]
      have : h₀f.meromorphicAt.order = n := by
        rw [MeromorphicAt.order_eq_int_iff (StronglyMeromorphicAt.meromorphicAt h₀f) n]
        use g
        constructor
        · assumption
        · constructor
          · assumption
          · exact eventually_nhdsWithin_of_eventually_nhds h₃g
      by_cases h₃f : h₀f.meromorphicAt.order = 0
      · simp [h₃f]
        have hn : n = (0 : ℤ) := by
          rw [h₃f] at this
          exact WithTop.coe_eq_zero.mp (id (Eq.symm this))
        simp_rw [hn]
        simp
        let t₀ : h₀f.meromorphicAt.order = (0 : ℤ) := by
          exact h₃f
        let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀
        have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by
          obtain ⟨h₀, h₁, h₂⟩  := Classical.choose_spec A
          apply localIdentity h₁g h₀
          rw [hn] at h₃g
          simp at h₃g
          simp at h₂
          have h₄g : f =ᶠ[𝓝[≠] z₀] g := by
            apply Filter.EventuallyEq.filter_mono h₃g
            exact nhdsWithin_le_nhds
          exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₄g) h₂
        exact Filter.EventuallyEq.eq_of_nhds this
      · simp [h₃f]
        left
        apply zero_zpow n
        by_contra hn
        rw [hn] at this
        tauto

  · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz