nevanlinna/Nevanlinna/stronglyMeromorphicOn.lean

import Nevanlinna.stronglyMeromorphicAt


open Topology


/- Strongly MeromorphicOn -/
def StronglyMeromorphicOn
  (f : ℂ → ℂ)
  (U : Set ℂ) :=
  ∀ z ∈ U, StronglyMeromorphicAt f z


/- Strongly MeromorphicAt is Meromorphic -/
theorem StronglyMeromorphicOn.meromorphicOn
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hf : StronglyMeromorphicOn f U) :
  MeromorphicOn f U := by
  intro z hz
  exact StronglyMeromorphicAt.meromorphicAt (hf z hz)


/- Strongly MeromorphicOn of non-negative order is analytic -/
theorem StronglyMeromorphicOn.analytic
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁f : StronglyMeromorphicOn f U)
  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
  ∀ z ∈ U, AnalyticAt ℂ f z := by
  intro z hz
  apply StronglyMeromorphicAt.analytic
  exact h₂f z hz
  exact h₁f z hz


/- Analytic functions are strongly meromorphic -/
theorem AnalyticOn.stronglyMeromorphicOn
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁f : AnalyticOn ℂ f U) :
  StronglyMeromorphicOn f U := by
  intro z hz
  apply AnalyticAt.stronglyMeromorphicAt
  let A := h₁f z hz
  exact h₁f z hz


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