nevanlinna/Nevanlinna/stronglyMeromorphicOn_eliminate.lean

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


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

lemma untop_eq_untop'
  {n : WithTop ℤ}
  (hn : n ≠ ⊤) :
  n.untop' 0 = n.untop hn := by
  rw [WithTop.untop'_eq_iff]
  simp


theorem MeromorphicOn.decompose₁
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (hz₀ : z₀ ∈ U)
  (h₁f : MeromorphicOn f U)
  (h₂f : StronglyMeromorphicAt f z₀)
  (h₃f : h₂f.meromorphicAt.order ≠ ⊤) :
  ∃ 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

  use g
  constructor
  · exact h₁g
  · constructor
    · apply h₂g.analytic


      sorry
    · constructor
      · sorry
      · sorry



theorem MeromorphicOn.decompose
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsConnected U)
  (h₂U : IsCompact U)
  (h₁f : MeromorphicOn f U)
  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
  ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
    ∧ (∀ z ∈ U, g z ≠ 0)
    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn ((∏ᶠ p, fun z ↦ (z - p) ^ (h₁f.divisor p)) * g) U) := by

  let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
  have h₁g₁ : MeromorphicOn g₁ U := by
    sorry
  let g := h₁g₁.makeStronglyMeromorphicOn
  have h₁g : MeromorphicOn g U := by
    sorry
  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
    sorry
  have h₃g : StronglyMeromorphicOn g U := by
    sorry
  have h₄g : AnalyticOnNhd ℂ g U := by
    intro z hz
    apply StronglyMeromorphicAt.analytic (h₃g z hz)
    rw [h₂g ⟨z, hz⟩]
  use g
  constructor
  · exact h₄g
  · constructor
    · intro z hz
      rw [← (h₄g z hz).order_eq_zero_iff]
      have A := (h₄g z hz).meromorphicAt_order
      rw [h₂g ⟨z, hz⟩] at A
      have t₀ : (h₄g z hz).order ≠ ⊤ := by
        by_contra hC
        rw [hC] at A
        tauto
      have t₁ : ∃ n : ℕ, (h₄g z hz).order = n := by
        exact Option.ne_none_iff_exists'.mp t₀
      obtain ⟨n, hn⟩ := t₁
      rw [hn] at A
      apply WithTopCoe
      rw [eq_comm]
      rw [hn]
      exact A
    · intro z hz
      have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by
        sorry
      have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by
        sorry
      have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
        sorry
      apply Filter.EventuallyEq.eq_of_nhds
      apply StronglyMeromorphicAt.localIdentity
      · exact StronglyMeromorphicOn_of_makeStronglyMeromorphic h₁f z hz
      · right
        use h₁f.divisor z
        use (∏ᶠ p : ({z}ᶜ : Set ℂ), (fun x ↦ (x - p.1) ^ h₁f.divisor p.1)) * g
        constructor
        · apply AnalyticAt.mul₁
          · apply analyticAt_finprod
            intro w


            sorry
          · apply (h₃g z hz).analytic
            rw [h₂g ⟨z, hz⟩]
        · constructor
          · sorry
          · sorry

      sorry