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.intervalIntegrability
import Nevanlinna.logpos
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.specialFunctions_CircleIntegral_affine
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.stronglyMeromorphicOn_eliminate
import Nevanlinna.mathlibAddOn

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral


theorem MeromorphicOn.integrable_log_abs_f₀
  {f : ℂ → ℂ}
  {r : ℝ}
  -- WARNING: Not optimal. This needs to go
  (hr : 0 < r)
  -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere
  (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) :
  IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by

  by_cases h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤
  · 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

    -- This is where we use 'ball' instead of sphere. However, better
    -- results should make this assumption unnecessary.
    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]
    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

    apply intervalIntegrable_logAbs_circleMap_sub_const
    exact Ne.symm (ne_of_lt hr)

  · push_neg at h₂f

    let F := h₁f.makeStronglyMeromorphicOn
    have : (fun z => log ‖f z‖) =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 r)] (fun z => log ‖F z‖) := by
      -- WANT: apply Filter.eventuallyEq.congr
      let A := (makeStronglyMeromorphicOn_changeDiscrete'' h₁f)
      obtain ⟨s, h₁s, h₂s⟩ := eventuallyEq_iff_exists_mem.1 A
      rw [eventuallyEq_iff_exists_mem]
      use s
      constructor
      · exact h₁s
      · intro x hx
        simp_rw [h₂s hx]
    have hU : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall 0 r := by
      rw [abs_of_pos hr]
      exact Metric.sphere_subset_closedBall
    have t₀ : (fun z => log ‖f (circleMap 0 r z)‖) =  (fun z => log ‖f z‖) ∘ circleMap 0 r := by
      rfl
    rw [t₀]
    clear t₀
    rw [integrability_congr_changeDiscrete hU this]

    have : ∀ x ∈ Metric.closedBall 0 r, F x = 0 := by
      intro x hx
      let A := h₂f ⟨x, hx⟩
      rw [← makeStronglyMeromorphicOn_changeOrder h₁f hx] at A
      let B := ((stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁f) x hx).order_eq_zero_iff.not.1
      simp [A] at B
      assumption
    have : (fun z => log ‖F z‖) ∘ circleMap 0 r = 0 := by
      funext x
      simp
      left
      apply this
      simp [abs_of_pos hr]
    simp_rw [this]
    apply intervalIntegral.intervalIntegrable_const


theorem MeromorphicOn.integrable_log_abs_f
  {f : ℂ → ℂ}
  {r : ℝ}
  -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere
  (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) |r|)) :
  IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by

  by_cases h₁r : r = 0
  · rw [h₁r]
    simp
  · by_cases h₂r : 0 < r
    · have : |r| = r := by
        exact abs_of_pos h₂r
      rw [this] at h₁f
      exact MeromorphicOn.integrable_log_abs_f₀ h₂r h₁f
    · have t₀ : 0 < -r := by
        have hr_neg : r < 0 := by
          apply lt_of_le_of_ne
          exact le_of_not_lt h₂r
          exact h₁r
        linarith
      have : |r| = -r := by
        apply abs_of_neg
        exact Left.neg_pos_iff.mp t₀
      rw [this] at h₁f
      let A := MeromorphicOn.integrable_log_abs_f₀ t₀ h₁f

      let B := integrability_congr_negRadius (f := fun z => log ‖f z‖) (r := -r)
      let C := B A
      simp at C
      simpa


theorem MeromorphicOn.integrable_logpos_abs_f
  {f : ℂ → ℂ}
  {r : ℝ}
  -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere
  (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) |r|)) :
  IntervalIntegrable (fun z ↦ logpos ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by

  simp_rw [logpos_norm]
  simp_rw [mul_add]

  apply IntervalIntegrable.add
  apply IntervalIntegrable.const_mul
  exact MeromorphicOn.integrable_log_abs_f h₁f

  apply IntervalIntegrable.const_mul
  apply IntervalIntegrable.norm
  exact MeromorphicOn.integrable_log_abs_f h₁f