nevanlinna/Nevanlinna/meromorphicAt.lean

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


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral


theorem meromorphicAt_congr
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩


theorem meromorphicAt_congr'
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)


theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  (∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by

  obtain ⟨n, h⟩ := hf
  let A := h.eventually_eq_zero_or_eventually_ne_zero

  rw [eventually_nhdsWithin_iff]
  rw [eventually_nhds_iff]
  rcases A with h₁|h₂
  · rw [eventually_nhds_iff] at h₁
    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
    left
    use N
    constructor
    · intro y h₁y h₂y
      let A := h₁N y h₁y
      simp at A
      rcases A with h₃|h₄
      · let B := h₃.1
        simp at h₂y
        let C := sub_eq_zero.1 B
        tauto
      · assumption
    · constructor
      · exact h₂N
      · exact h₃N
  · right
    rw [eventually_nhdsWithin_iff]
    rw [eventually_nhds_iff]
    rw [eventually_nhdsWithin_iff] at h₂
    rw [eventually_nhds_iff] at h₂
    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
    use N
    constructor
    · intro y h₁y h₂y
      by_contra h
      let A := h₁N y h₁y h₂y
      rw [h] at A
      simp at A
    · constructor
      · exact h₂N
      · exact h₃N


theorem MeromorphicAt.order_congr
  {f₁ f₂ : ℂ → ℂ}
  {z₀ : ℂ}
  (hf₁ : MeromorphicAt f₁ z₀)
  (h : f₁ =ᶠ[𝓝[≠] z₀] f₂):
  hf₁.order = (hf₁.congr h).order := by
  by_cases hord : hf₁.order = ⊤
  · rw [hord, eq_comm]
    rw [hf₁.order_eq_top_iff] at hord
    rw [(hf₁.congr h).order_eq_top_iff]
    exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
  · obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn
    rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff]
    use g
    constructor
    · assumption
    · constructor
      · assumption
      · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))


theorem MeromorphicAt.order_mul
  {f₁ f₂ : ℂ → ℂ}
  {z₀ : ℂ}
  (hf₁ : MeromorphicAt f₁ z₀)
  (hf₂ : MeromorphicAt f₂ z₀) :
  (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
  by_cases h₂f₁ : hf₁.order = ⊤
  · simp [h₂f₁]
    rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁
    rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
    use t
    constructor
    · intro y h₁y h₂y
      simp; left
      rw [h₁t y h₁y h₂y]
    · exact ⟨h₂t, h₃t⟩
  · by_cases h₂f₂ : hf₂.order = ⊤
    · simp [h₂f₂]
      rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂
      rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
      use t
      constructor
      · intro y h₁y h₂y
        simp; right
        rw [h₁t y h₁y h₂y]
      · exact ⟨h₂t, h₃t⟩
    · have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁)
      have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂)
      obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁
      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂
      rw [h₃f₁, h₃f₂, ← WithTop.coe_add]
      rw [MeromorphicAt.order_eq_int_iff]
      use g₁ * g₂
      constructor
      · exact AnalyticAt.mul h₁g₁ h₁g₂
      · constructor
        · simp; tauto
        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁)
          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂)
          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
          use t₁ ∩ t₂
          constructor
          · intro y h₁y h₂y
            simp
            rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y]
            simp
            rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
            group
          · constructor
            · exact IsOpen.inter h₂t₁ h₂t₂
            · exact Set.mem_inter h₃t₁ h₃t₂


-- might want theorem MeromorphicAt.order_zpow