nevanlinna/Nevanlinna/meromorphicOn_decompose.lean

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


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

lemma WithTopCoe
  {n : WithTop ℕ} :
  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
  rcases n with h|h
  · intro h
    contradiction
  · intro h₁
    simp only [WithTop.map, Option.map] at h₁
    have : (h : ℤ) = 0 := by
      exact WithTop.coe_eq_zero.mp h₁
    have : h = 0 := by
      exact Int.ofNat_eq_zero.mp this
    rw [this]
    rfl


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 (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) 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

      sorry