nevanlinna/Nevanlinna/stronglyMeromorphicOn.lean

import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicAt
import Mathlib.Algebra.BigOperators.Finprod

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 : AnalyticOnNhd ℂ f U) :
  StronglyMeromorphicOn f U := by
  intro z hz
  apply AnalyticAt.stronglyMeromorphicAt
  exact h₁f z hz


/- Make strongly MeromorphicAt -/
noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hf : MeromorphicOn f U) :
  ℂ → ℂ := by
  intro z
  by_cases hz : z ∈ U
  · exact (hf z hz).makeStronglyMeromorphicAt z
  · exact f z


theorem makeStronglyMeromorphicOn_changeDiscrete
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicOn f U)
  (hz₀ : z₀ ∈ U) :
  hf.makeStronglyMeromorphicOn =ᶠ[𝓝[≠] z₀] f := by
  apply Filter.eventually_iff_exists_mem.2
  let A := (hf z₀ hz₀).eventually_analyticAt
  obtain ⟨V, h₁V, h₂V⟩  := Filter.eventually_iff_exists_mem.1 A
  use V
  constructor
  · assumption
  · intro v hv
    unfold MeromorphicOn.makeStronglyMeromorphicOn
    by_cases h₂v : v ∈ U
    · simp [h₂v]
      rw [← StronglyMeromorphicAt.makeStronglyMeromorphic_id]
      exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
    · simp [h₂v]


theorem analyticAt_ratlPolynomial₁
  {z : ℂ}
  (d : ℂ → ℤ)
  (P : Finset ℂ) :
  z ∉ P → AnalyticAt ℂ (∏ u ∈ P, fun z ↦ (z - u) ^ d u) z := by
  intro hz
  rw [Finset.prod_fn]
  apply Finset.analyticAt_prod
  intro u hu
  apply AnalyticAt.zpow
  apply AnalyticAt.sub
  apply analyticAt_id
  apply analyticAt_const
  rw [sub_ne_zero, ne_comm]
  exact ne_of_mem_of_not_mem hu hz


theorem stronglyMeromorphicOn_ratlPolynomial₂
  {U : Set ℂ}
  (d : ℂ → ℤ)
  (P : Finset ℂ) :
  StronglyMeromorphicOn (∏ u ∈ P, fun z ↦ (z - u) ^ d u) U := by

  intro z hz
  by_cases h₂z : z ∈ P
  · rw [← Finset.mul_prod_erase P _ h₂z]
    right
    use d z
    use ∏ x ∈ P.erase z, fun z => (z - x) ^ d x
    constructor
    · have : z ∉ P.erase z := Finset.not_mem_erase z P
      apply analyticAt_ratlPolynomial₁ d (P.erase z) this
    · constructor
      · simp only [Finset.prod_apply]
        rw [Finset.prod_ne_zero_iff]
        intro u hu
        apply zpow_ne_zero
        rw [sub_ne_zero]
        by_contra hCon
        rw [hCon] at hu
        let A := Finset.not_mem_erase u P
        tauto
      · exact Filter.Eventually.of_forall (congrFun rfl)
  · apply AnalyticAt.stronglyMeromorphicAt
    exact analyticAt_ratlPolynomial₁ d P (z := z) h₂z



theorem stronglyMeromorphicOn_ratlPolynomial₃
  {U : Set ℂ}
  (d : ℂ → ℤ) :
  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
  by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite
  · rw [finprod_eq_prod _ hd]
    apply stronglyMeromorphicOn_ratlPolynomial₂ (U := U) d hd.toFinset
  · rw [finprod_of_infinite_mulSupport hd]
    apply AnalyticOn.stronglyMeromorphicOn
    apply analyticOnNhd_const


theorem stronglyMeromorphicOn_divisor_ratlPolynomial
  {U : Set ℂ}
  (d : ℂ → ℤ)
  (hd : Set.Finite d.support) :
  (stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
  sorry


theorem makeStronglyMeromorphicOn_changeDiscrete'
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicOn f U)
  (hz₀ : z₀ ∈ U) :
  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
  apply Mnhds
  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
  apply Filter.EventuallyEq.trans A
  exact m₂ (hf z₀ hz₀)
  unfold MeromorphicOn.makeStronglyMeromorphicOn
  simp [hz₀]


theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hf : MeromorphicOn f U) :
  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
  intro z₀ hz₀
  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)