nevanlinna/Nevanlinna/meromorphicOn_integrability.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Mathlib.MeasureTheory.Integral.CircleIntegral
import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Nevanlinna.analyticAt
import Nevanlinna.divisor
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.stronglyMeromorphicOn_eliminate
import Nevanlinna.mathlibAddOn

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral


/- Integral and Integrability up to changes on codiscrete sets -/

theorem d
  {U S : Set ℂ}
  {c : ℂ}
  {r : ℝ}
  (hr : r ≠ 0)
  (hU : Metric.sphere c |r| ⊆ U)
  (hS : S ∈ Filter.codiscreteWithin U) :
  Countable ((circleMap c r)⁻¹' Sᶜ) := by

  have : (circleMap c r)⁻¹' (S ∪ Uᶜ)ᶜ = (circleMap c r)⁻¹' Sᶜ := by
    simp [(by simpa : (circleMap c r)⁻¹' U = ⊤)]
  rw [← this]

  apply Set.Countable.preimage_circleMap _ c hr
  have : DiscreteTopology ((S ∪ Uᶜ)ᶜ : Set ℂ) := by
    rw [discreteTopology_subtype_iff]
    rw [mem_codiscreteWithin] at hS; simp at hS

    intro x hx
    rw [← mem_iff_inf_principal_compl, (by ext z; simp; tauto : S ∪ Uᶜ = (U \ S)ᶜ)]
    rw [Set.compl_union, compl_compl] at hx
    exact hS x hx.2

  apply TopologicalSpace.separableSpace_iff_countable.1
  exact TopologicalSpace.SecondCountableTopology.to_separableSpace


theorem integrability_congr_changeDiscrete₀
  {f₁ f₂ : ℂ → ℝ}
  {U : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere 0 |r| ⊆ U)
  (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) :
  IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) → IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by
  intro hf₁

  by_cases hr : r = 0
  · unfold circleMap
    rw [hr]
    simp
    have : f₂ ∘ (fun (θ : ℝ) ↦ 0) = (fun r ↦ f₂ 0) := by
      exact rfl
    rw [this]
    simp

  · apply IntervalIntegrable.congr hf₁
    rw [Filter.eventuallyEq_iff_exists_mem]
    use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z}
    constructor
    · apply Set.Countable.measure_zero (d hr hU hf)
    · tauto


theorem integrability_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℝ}
  {U : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere (0 : ℂ) |r| ⊆ U)
  (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) :
  IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) ↔ IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by

  constructor
  · exact integrability_congr_changeDiscrete₀ hU hf
  · exact integrability_congr_changeDiscrete₀ hU (EventuallyEq.symm hf)


theorem integral_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℝ}
  {U : Set ℂ}
  {r : ℝ}
  (hr : r ≠ 0)
  (hU : Metric.sphere 0 |r| ⊆ U)
  (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) :
  ∫ (x : ℝ) in (0)..(2 * π), f₁ (circleMap 0 r x) = ∫ (x : ℝ) in (0)..(2 * π), f₂ (circleMap 0 r x) := by

  apply intervalIntegral.integral_congr_ae
  rw [eventually_iff_exists_mem]
  use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z}
  constructor
  · apply Set.Countable.measure_zero (d hr hU hf)
  · tauto


theorem MeromorphicOn.integrable_log_abs_f
  {f : ℂ → ℂ}
  {r : ℝ}
  (hr : 0 < r)
  (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r))
  (h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤) :
  IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by

  have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := isCompact_closedBall 0 r

  have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by
    constructor
    · exact Metric.nonempty_closedBall.mpr (le_of_lt hr)
    · exact (convex_closedBall (0 : ℂ) r).isPreconnected

  have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by
    rw [interior_closedBall, ← Set.nonempty_iff_ne_empty]
    use 0; simp [hr];
    repeat exact Ne.symm (ne_of_lt hr)

  have h₃f : Set.Finite (Function.support h₁f.divisor) := by
    exact Divisor.finiteSupport h₁U h₁f.divisor

  obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f
  have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by
    rfl
  rw [this]
  have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by
    rw [abs_of_pos hr]
    apply Metric.sphere_subset_closedBall

  rw [integrability_congr_changeDiscrete this h₃g]

  apply IntervalIntegrable.add
  --
  apply Continuous.intervalIntegrable
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => log ‖g (circleMap 0 r x)‖) = log ∘ Complex.abs ∘ g ∘ (fun x ↦ circleMap 0 r x) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  apply Real.continuousAt_log
  · simp
    have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by
      apply circleMap_mem_closedBall
      exact le_of_lt hr
    exact h₂g ⟨(circleMap 0 r x), this⟩
  apply ContinuousAt.comp
  · apply Continuous.continuousAt Complex.continuous_abs
  apply ContinuousAt.comp
  · have : (circleMap 0 r x) ∈ (Metric.closedBall (0 : ℂ) r) := by
      apply circleMap_mem_closedBall (0 : ℂ) (le_of_lt hr) x
    apply (h₁g (circleMap 0 r x) this).continuousAt
  apply Continuous.continuousAt (continuous_circleMap 0 r)
  --
  have h {x : ℝ} : (Function.support fun s => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) ⊆ h₃f.toFinset := by
    intro x; simp; tauto
  simp_rw [finsum_eq_sum_of_support_subset _ h]
  --let A := IntervalIntegrable.sum h₃f.toFinset
  --have h : ∀ s ∈ h₃f.toFinset, IntervalIntegrable (f i) volume 0 (2 * π) := by
  --  sorry
  have : (fun x => ∑ s ∈ h₃f.toFinset, (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) = (∑ s ∈ h₃f.toFinset, fun x => (h₁f.divisor s) * log ‖circleMap 0 r x - s‖) := by
    ext x; simp
  rw [this]
  apply IntervalIntegrable.sum h₃f.toFinset
  intro s hs
  apply IntervalIntegrable.const_mul

  sorry