nevanlinna/Nevanlinna/stronglyMeromorphicOn_eliminate.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.divisor
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.stronglyMeromorphicOn_ratlPolynomial
import Nevanlinna.mathlibAddOn

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

theorem MeromorphicOn.decompose₁
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (h₁f : MeromorphicOn f U)
  (h₂f : StronglyMeromorphicAt f z₀)
  (h₃f : h₂f.meromorphicAt.order ≠ ⊤)
  (hz₀ : z₀ ∈ U) :
  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
    ∧ (AnalyticAt ℂ g z₀)
    ∧ (g z₀ ≠ 0)
    ∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by

  let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀)
  have h₁h₁ : MeromorphicOn h₁ U := by
    apply MeromorphicOn.zpow
    apply AnalyticOnNhd.meromorphicOn
    apply AnalyticOnNhd.sub
    exact analyticOnNhd_id
    exact analyticOnNhd_const
  let n : ℤ := (-h₁f.divisor z₀)
  have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by
    simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff]
    use 1
    constructor
    · apply analyticAt_const
    · constructor
      · simp
      · apply eventually_nhdsWithin_of_forall
        intro z hz
        simp

  let g₁ := f * h₁
  have h₁g₁ : MeromorphicOn g₁ U := by
    apply h₁f.mul h₁h₁
  have h₂g₁ : (h₁g₁ z₀ hz₀).order = 0 := by
    rw [(h₁f z₀ hz₀).order_mul (h₁h₁ z₀ hz₀)]
    rw [h₂h₁]
    unfold n
    rw [MeromorphicOn.divisor_def₂ h₁f hz₀ h₃f]
    conv =>
      left
      left
      rw [Eq.symm (WithTop.coe_untop (h₁f z₀ hz₀).order h₃f)]
    have
      (a b c : ℤ)
      (h : a + b = c) :
      (a : WithTop ℤ) + (b : WithTop ℤ) = (c : WithTop ℤ) := by
      rw [← h]
      simp
    rw [this ((h₁f z₀ hz₀).order.untop h₃f) (-(h₁f z₀ hz₀).order.untop h₃f) 0]
    simp
    ring

  let g := (h₁g₁ z₀ hz₀).makeStronglyMeromorphicAt
  have h₂g : StronglyMeromorphicAt g z₀ := by
    exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (h₁g₁ z₀ hz₀)
  have h₁g : MeromorphicOn g U := by
    intro z hz
    by_cases h₁z : z = z₀
    · rw [h₁z]
      apply h₂g.meromorphicAt
    · apply (h₁g₁ z hz).congr
      rw [eventuallyEq_nhdsWithin_iff]
      rw [eventually_nhds_iff]
      use {z₀}ᶜ
      constructor
      · intro y h₁y h₂y
        let A := m₁ (h₁g₁ z₀ hz₀) y h₁y
        unfold g
        rw [← A]
      · constructor
        · exact isOpen_compl_singleton
        · exact h₁z
  have h₃g : (h₁g z₀ hz₀).order = 0 := by
    unfold g
    let B := m₂ (h₁g₁ z₀ hz₀)
    let A := (h₁g₁ z₀ hz₀).order_congr B
    rw [← A]
    rw [h₂g₁]
  have h₄g : AnalyticAt ℂ g z₀ := by
    apply h₂g.analytic
    rw [h₃g]

  use g
  constructor
  · exact h₁g
  · constructor
    · exact h₄g
    · constructor
      · exact (h₂g.order_eq_zero_iff).mp h₃g
      · funext z
        by_cases hz : z = z₀
        · rw [hz]
          simp
          by_cases h : h₁f.divisor z₀ = 0
          · simp [h]
            have h₂h₁ : h₁ = 1 := by
              funext w
              unfold h₁
              simp [h]
            have h₃g₁ : g₁ = f := by
              unfold g₁
              rw [h₂h₁]
              simp
            have h₄g₁ : StronglyMeromorphicAt g₁ z₀ := by
              rwa [h₃g₁]
            let A := h₄g₁.makeStronglyMeromorphic_id
            unfold g
            rw [← A, h₃g₁]
          · have : (0 : ℂ) ^ h₁f.divisor z₀ = (0 : ℂ) := by
              exact zero_zpow (h₁f.divisor z₀) h
            rw [this]
            simp
            let A := h₂f.order_eq_zero_iff.not
            simp at A
            rw [← A]
            unfold MeromorphicOn.divisor at h
            simp [hz₀] at h
            exact h.1
        · simp
          let B := m₁ (h₁g₁ z₀ hz₀) z hz
          unfold g
          rw [← B]
          unfold g₁ h₁
          simp [hz]
          rw [mul_assoc]
          rw [inv_mul_cancel₀]
          simp
          apply zpow_ne_zero
          rwa [sub_ne_zero]


theorem MeromorphicOn.decompose₂
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {P : Finset U}
  (hf : StronglyMeromorphicOn f U) :
  (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
    ∃ g : ℂ → ℂ, (MeromorphicOn g U)
    ∧ (∀ p : P, AnalyticAt ℂ g p)
    ∧ (∀ p : P, g p ≠ 0)
    ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by

  apply Finset.induction (p := fun (P : Finset U) ↦
    (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
    ∃ g : ℂ → ℂ, (MeromorphicOn g U)
    ∧ (∀ p : P, AnalyticAt ℂ g p)
    ∧ (∀ p : P, g p ≠ 0)
    ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)))

  -- case empty
  simp
  exact hf.meromorphicOn

  -- case insert
  intro u P hu iHyp
  intro hOrder
  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀, h₄g₀⟩ := iHyp (fun p hp ↦ hOrder p (Finset.mem_insert_of_mem hp))

  have h₀ : AnalyticAt ℂ (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u := by
    have : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) = (fun z => ∏ p : P, (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
      funext w
      simp
    rw [this]
    apply Finset.analyticAt_prod
    intro p hp
    apply AnalyticAt.zpow
    apply AnalyticAt.sub
    apply analyticAt_id
    apply analyticAt_const
    by_contra hCon
    rw [sub_eq_zero] at hCon
    have : p.1 = u := by
      exact SetCoe.ext (_root_.id (Eq.symm hCon))
    rw [← this] at hu
    simp [hp] at hu

  have h₁ : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u ≠ 0 := by
    simp only [Finset.prod_apply]
    rw [Finset.prod_ne_zero_iff]
    intro p hp
    apply zpow_ne_zero
    by_contra hCon
    rw [sub_eq_zero] at hCon
    have : p.1 = u := by
      exact SetCoe.ext (_root_.id (Eq.symm hCon))
    rw [← this] at hu
    simp [hp] at hu

  have h₅g₀ : StronglyMeromorphicAt g₀ u := by
    rw [stronglyMeromorphicAt_of_mul_analytic h₀ h₁]
    rw [← h₄g₀]
    exact hf u u.2

  have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by
    by_contra hCon
    let A := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
    simp_rw [← h₄g₀, hCon] at A
    simp at A
    let B := hOrder u (Finset.mem_insert_self u P)
    tauto

  obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁g₀.decompose₁ h₅g₀ h₆g₀ u.2
  use g
  · constructor
    · exact h₁g
    · constructor
      · intro ⟨v₁, v₂⟩
        simp
        simp at v₂
        rcases v₂ with hv|hv
        · rwa [hv]
        · let A := h₂g₀ ⟨v₁, hv⟩
          rw [h₄g] at A
          rw [← analyticAt_of_mul_analytic] at A
          simp at A
          exact A
          --
          simp
          apply AnalyticAt.zpow
          apply AnalyticAt.sub
          apply analyticAt_id
          apply analyticAt_const
          by_contra hCon
          rw [sub_eq_zero] at hCon

          have : v₁ = u := by
            exact SetCoe.ext hCon
          rw [this] at hv
          tauto
          --
          apply zpow_ne_zero
          simp
          by_contra hCon
          rw [sub_eq_zero] at hCon
          have : v₁ = u := by
            exact SetCoe.ext hCon
          rw [this] at hv
          tauto

      · constructor
        · intro ⟨v₁, v₂⟩
          simp
          simp at v₂
          rcases v₂ with hv|hv
          · rwa [hv]
          · by_contra hCon
            let A := h₃g₀ ⟨v₁,hv⟩
            rw [h₄g] at A
            simp at A
            tauto
        · conv =>
            left
            rw [h₄g₀, h₄g]
          simp
          rw [mul_assoc]
          congr
          rw [Finset.prod_insert]
          simp
          congr
          have : (hf u u.2).meromorphicAt.order = (h₁g₀ u u.2).order := by
            have h₅g₀ : f =ᶠ[𝓝 u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
              exact Eq.eventuallyEq h₄g₀
            have h₆g₀ : f =ᶠ[𝓝[≠] u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
              exact eventuallyEq_nhdsWithin_of_eqOn fun ⦃x⦄ a => congrFun h₄g₀ x
            rw [(hf u u.2).meromorphicAt.order_congr h₆g₀]
            let C := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
            rw [C]
            let D := h₀.order_eq_zero_iff.2 h₁
            let E := h₀.meromorphicAt_order
            rw [E, D]
            simp
          have : hf.meromorphicOn.divisor u = h₁g₀.divisor u := by
            unfold MeromorphicOn.divisor
            simp
            rw [this]
          rw [this]
          --
          simpa



theorem MeromorphicOn.decompose₃'
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsCompact U)
  (h₂U : IsConnected U)
  (h₁f : StronglyMeromorphicOn f U)
  (h₂f : ∃ u : U, f u ≠ 0) :
  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
    ∧ (AnalyticOn ℂ g U)
    ∧ (∀ u : U, g u ≠ 0)
    ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by

  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f
  have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U

  let d := - h₁f.meromorphicOn.divisor.toFun
  have h₁d : d.support = (Function.support h₁f.meromorphicOn.divisor) := by
    ext x
    unfold d
    simp
  let h₁ := ∏ᶠ u, fun z ↦ (z - u) ^ (d u)
  have h₁h₁ : StronglyMeromorphicOn h₁ U := by
    intro z hz
    exact stronglyMeromorphicOn_ratlPolynomial₃ d z trivial
  have h₂h₁ : h₁h₁.meromorphicOn.divisor = d := by
    apply stronglyMeromorphicOn_divisor_ratlPolynomial_U
    rwa [h₁d]
    --
    rw [h₁d]
    exact (StronglyMeromorphicOn.meromorphicOn h₁f).divisor.supportInU
  have h₃h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order ≠ ⊤ := by
    intro z hz
    apply stronglyMeromorphicOn_ratlPolynomial₃order
  have h₄h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order = d z := by
    intro z hz
    rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁]
    rwa [h₁d]

  let g' := f * h₁
  have h₁g' : MeromorphicOn g' U := h₁f.meromorphicOn.mul h₁h₁.meromorphicOn
  have h₂g' : h₁g'.divisor.toFun = 0 := by
    rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn h₃h₁]
    rw [h₂h₁]
    unfold d
    simp
  have h₃g' : ∀ u : U, (h₁g' u.1 u.2).order = 0 := by
    intro u
    rw [(h₁f u.1 u.2).meromorphicAt.order_mul (h₁h₁ u.1 u.2).meromorphicAt]
    rw [h₄h₁]
    unfold d
    unfold MeromorphicOn.divisor
    simp
    have : (h₁f u.1 u.2).meromorphicAt.order = WithTop.untop' 0 (h₁f u.1 u.2).meromorphicAt.order := by
      rw [eq_comm]
      let A := h₃f u
      exact untop'_of_ne_top A
    rw [this]
    simp
    rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
    rw [← WithTop.coe_add]
    simp
    exact u.2

  let g := h₁g'.makeStronglyMeromorphicOn
  have h₁g : StronglyMeromorphicOn g U := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁g'
  have h₂g : h₁g.meromorphicOn.divisor.toFun = 0 := by
    rw [← MeromorphicOn.divisor_of_makeStronglyMeromorphicOn]
    rw [h₂g']
  have h₃g : AnalyticOnNhd ℂ g U := by
    apply StronglyMeromorphicOn.analyticOnNhd
    rw [h₂g]
    simp
    assumption
  have h₄g : ∀ u : U, g u ≠ 0 := by
    intro u
    rw [← (h₁g u.1 u.2).order_eq_zero_iff]
    rw [makeStronglyMeromorphicOn_changeOrder]
    let A := h₃g' u
    exact A
    exact u.2

  use g
  constructor
  · exact StronglyMeromorphicOn.meromorphicOn h₁g
  · constructor
    · exact AnalyticOnNhd.analyticOn h₃g
    · constructor
      · exact h₄g
      · have t₀ : StronglyMeromorphicOn (g * ∏ᶠ (u : ℂ), fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) U := by
          apply stronglyMeromorphicOn_of_mul_analytic' h₃g h₄g
          apply stronglyMeromorphicOn_ratlPolynomial₃U

        funext z
        by_cases hz : z ∈ U
        · apply Filter.EventuallyEq.eq_of_nhds
          apply StronglyMeromorphicAt.localIdentity (h₁f z hz) (t₀ z hz)
          have h₅g : g =ᶠ[𝓝[≠] z] g' := makeStronglyMeromorphicOn_changeDiscrete h₁g' hz
          have Y' : (g' * ∏ᶠ (u : ℂ), fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) =ᶠ[𝓝[≠] z] g * ∏ᶠ (u : ℂ), fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u) := by
            apply Filter.EventuallyEq.symm
            exact Filter.EventuallyEq.mul h₅g (by simp)
          apply Filter.EventuallyEq.trans _ Y'
          unfold g'
          unfold h₁

          let A := h₁f.meromorphicOn.divisor.locallyFiniteInU z hz
          let B := eventually_nhdsWithin_iff.1 A
          obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 B

          apply eventually_nhdsWithin_iff.2
          rw [eventually_nhds_iff]
          use t
          constructor
          · intro y h₁y h₂y
            let C := h₁t y h₁y h₂y
            rw [mul_assoc]
            simp
            have : (finprod (fun u z => (z - u) ^ d u) y * finprod (fun u z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) y) = 1 := by
              have t₀ : (Function.mulSupport fun u z => (z - u) ^ d u).Finite := by
                rwa [ratlPoly_mulsupport, h₁d]
              rw [finprod_eq_prod _ t₀]
              have t₁ : (Function.mulSupport fun u z => (z - u) ^ h₁f.meromorphicOn.divisor u).Finite := by
                rwa [ratlPoly_mulsupport]
              rw [finprod_eq_prod _ t₁]
              have : (Function.mulSupport fun u z => (z - u) ^ d u) = (Function.mulSupport fun u z => (z - u) ^ h₁f.meromorphicOn.divisor u) := by
                rw [ratlPoly_mulsupport]
                rw [ratlPoly_mulsupport]
                unfold d
                simp
              have : t₀.toFinset = t₁.toFinset := by congr
              rw [this]
              simp
              rw [← Finset.prod_mul_distrib]
              apply Finset.prod_eq_one
              intro x hx
              apply zpow_neg_mul_zpow_self
              have : y ∉ t₁.toFinset := by
                simp
                simp at C
                rw [C]
                simp
                tauto
              by_contra H
              rw [sub_eq_zero] at H
              rw [H] at this
              tauto

            rw [this]
            simp
          · exact ⟨h₂t, h₃t⟩
        · simp
          have : g z = g' z := by
            unfold g
            unfold MeromorphicOn.makeStronglyMeromorphicOn
            simp [hz]
          rw [this]
          unfold g'
          unfold h₁
          simp
          rw [mul_assoc]
          nth_rw 1 [← mul_one (f z)]
          congr
          have t₀ : (Function.mulSupport fun u z => (z - u) ^ d u).Finite := by
            rwa [ratlPoly_mulsupport, h₁d]
          rw [finprod_eq_prod _ t₀]
          have t₁ : (Function.mulSupport fun u z => (z - u) ^ h₁f.meromorphicOn.divisor u).Finite := by
            rwa [ratlPoly_mulsupport]
          rw [finprod_eq_prod _ t₁]
          have : (Function.mulSupport fun u z => (z - u) ^ d u) = (Function.mulSupport fun u z => (z - u) ^ h₁f.meromorphicOn.divisor u) := by
            rw [ratlPoly_mulsupport]
            rw [ratlPoly_mulsupport]
            unfold d
            simp
          have : t₀.toFinset = t₁.toFinset := by congr
          rw [this]
          simp
          rw [← Finset.prod_mul_distrib]
          rw [eq_comm]
          apply Finset.prod_eq_one
          intro x hx
          apply zpow_neg_mul_zpow_self

          have : z ∉ t₁.toFinset := by
            simp
            have : h₁f.meromorphicOn.divisor z = 0 := by
              let A := h₁f.meromorphicOn.divisor.supportInU
              simp at A
              by_contra H
              let B := A z H
              tauto
            rw [this]
            simp
            rfl
          by_contra H
          rw [sub_eq_zero] at H
          rw [H] at this
          tauto