nevanlinna/Nevanlinna/stronglyMeromorphic_JensenFormula.lean

import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.analyticOnNhd_zeroSet
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
import Nevanlinna.specialFunctions_CircleIntegral_affine
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.stronglyMeromorphicOn_eliminate
import Nevanlinna.meromorphicOn_divisor

open Real



theorem jensen_case_R_eq_one
  (f : ℂ → ℂ)
  (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1))
  (h₂f : f 0 ≠ 0) :
  log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by

  have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by
    constructor
    · refine Metric.nonempty_closedBall.mpr (by simp)
    · exact (convex_closedBall (0 : ℂ) 1).isPreconnected

  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
    isCompact_closedBall 0 1

  have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
    use ⟨0, Metric.mem_closedBall_self (by simp)⟩

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

  have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by
    intro x
    contrapose
    simp
    intro hx
    rw [hx]
    simp
  rw [finsum_eq_sum_of_support_subset _ h₄f]

  obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f h'₂f

  have h₁F : Function.mulSupport (fun u ↦ fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) ⊆ h₃f.toFinset := by
    intro u
    contrapose
    simp
    intro hu
    rw [hu]
    simp
    exact rfl
  rw [finprod_eq_prod_of_mulSupport_subset _ h₁F] at h₄F

  let G := fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖

  have h₁G {z : ℂ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) ⊆ h₃f.toFinset := by
    intro s
    contrapose
    simp
    intro hs
    rw [hs]
    simp

  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
    intro z h₁z h₂z

    rw [h₄F]
    simp only [Pi.mul_apply, norm_mul]
    simp only [Finset.prod_apply, norm_prod, norm_zpow]
    rw [Real.log_mul]
    rw [Real.log_prod]
    simp_rw [Real.log_zpow]
    dsimp only [G]
    rw [finsum_eq_sum_of_support_subset _ h₁G]
    --
    intro x hx
    simp at hx


    abel

    -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
      intro s hs
      simp at hs
      simp
      intro h₂s
      rw [h₂s] at h₂z
      tauto
    exact this

    -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
      intro s hs
      simp at hs
      simp
      intro h₂s
      rw [h₂s] at h₂z
      tauto
    rw [Finset.prod_ne_zero_iff]
    exact this

    -- Complex.abs (F z) ≠ 0
    simp
    exact h₂F z h₁z


  have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by

    rw [intervalIntegral.integral_congr_ae]
    rw [MeasureTheory.ae_iff]
    apply Set.Countable.measure_zero
    simp

    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
      intro a ha
      simp at ha
      simp
      by_contra C
      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
      exact ha.2 (decompose_f (circleMap 0 1 a) this C)

    apply Set.Countable.mono t₀
    apply Set.Countable.preimage_circleMap
    apply Set.Finite.countable
    let A := finiteZeros h₁U h₂U h₁f h'₂f

    have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
      ext z
      simp
      tauto
    rw [this]
    exact Set.Finite.image Subtype.val A
    exact Ne.symm (zero_ne_one' ℝ)


  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
    = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
        + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
    dsimp [G]
    rw [intervalIntegral.integral_add]
    rw [intervalIntegral.integral_finset_sum]
    simp_rw [intervalIntegral.integral_const_mul]

    --  ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
    --  IntervalIntegrable (fun x => (h'₁f.order i).toNat *
    --    log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
    intro i _
    apply IntervalIntegrable.const_mul
    --simp at this
    by_cases h₂i : ‖i.1‖ = 1
    -- case pos
    exact int'₂ h₂i
    -- case neg
    apply Continuous.intervalIntegrable
    apply continuous_iff_continuousAt.2
    intro x
    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
      rfl
    rw [this]
    apply ContinuousAt.comp
    apply Real.continuousAt_log
    simp

    by_contra ha'
    conv at h₂i =>
      arg 1
      rw [← ha']
      rw [Complex.norm_eq_abs]
      rw [abs_circleMap_zero 1 x]
      simp
    tauto
    apply ContinuousAt.comp
    apply Complex.continuous_abs.continuousAt
    fun_prop
    -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
    apply Continuous.intervalIntegrable
    apply continuous_iff_continuousAt.2
    intro x
    have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
      rfl
    rw [this]
    apply ContinuousAt.comp
    apply Real.continuousAt_log
    simp [h₂F]
    -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
    apply ContinuousAt.comp
    apply Complex.continuous_abs.continuousAt
    apply ContinuousAt.comp
    apply DifferentiableAt.continuousAt (𝕜 := ℂ )
    apply HolomorphicAt.differentiableAt
    simp [h'₁F]
    -- ContinuousAt (fun x => circleMap 0 1 x) x
    apply Continuous.continuousAt
    apply continuous_circleMap

    have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
      = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
      funext x
      simp
    rw [this]
    apply IntervalIntegrable.sum
    intro i _
    apply IntervalIntegrable.const_mul
    --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
    --simp at this
    by_cases h₂i : ‖i.1‖ = 1
    -- case pos
    exact int'₂ h₂i
    -- case neg
    --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
    apply Continuous.intervalIntegrable
    apply continuous_iff_continuousAt.2
    intro x
    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
      rfl
    rw [this]
    apply ContinuousAt.comp
    apply Real.continuousAt_log
    simp

    by_contra ha'
    conv at h₂i =>
      arg 1
      rw [← ha']
      rw [Complex.norm_eq_abs]
      rw [abs_circleMap_zero 1 x]
      simp
    tauto
    apply ContinuousAt.comp
    apply Complex.continuous_abs.continuousAt
    fun_prop

  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
    let logAbsF := fun w ↦ Real.log ‖F w‖
    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
      intro z hz
      apply logabs_of_holomorphicAt_is_harmonic
      apply h'₁F z hz
      exact h₂F z hz

    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀

  simp_rw [← Complex.norm_eq_abs] at decompose_int_G
  rw [t₁] at decompose_int_G

  conv at decompose_int_G =>
    right
    right
    arg 2
    intro x
    right
    rw [int₃ x.2]
  simp at decompose_int_G

  rw [int_logAbs_f_eq_int_G]
  rw [decompose_int_G]
  rw [h₃F]
  simp
  have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
    calc π⁻¹ * 2⁻¹ * (2 * π * l)
    _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
    _ = π⁻¹ * π * l := by ring
    _ = (π⁻¹ * π) * l := by ring
    _ = 1 * l := by
      rw [inv_mul_cancel₀]
      exact pi_ne_zero
    _ = l := by simp
  rw [this]
  rw [log_mul]
  rw [log_prod]
  simp

  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
  simp
  simp
  intro x ⟨h₁x, _⟩
  simp

  dsimp [AnalyticOnNhd.order] at h₁x
  simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
  exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x

  --
  intro x hx
  simp at hx
  simp
  intro h₁x
  nth_rw 1 [← h₁x] at h₂f
  tauto

  --
  rw [Finset.prod_ne_zero_iff]
  intro x hx
  simp at hx
  simp
  intro h₁x
  nth_rw 1 [← h₁x] at h₂f
  tauto

  --
  simp
  apply h₂F
  simp


lemma const_mul_circleMap_zero
  {R θ : ℝ} :
  circleMap 0 R θ = R * circleMap 0 1 θ := by
  rw [circleMap_zero, circleMap_zero]
  simp


theorem jensen
  {R : ℝ}
  (hR : 0 < R)
  (f : ℂ → ℂ)
  (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 R))
  (h₂f : f 0 ≠ 0) :
  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by


  let ℓ : ℂ ≃L[ℂ] ℂ :=
  {
    toFun := fun x ↦ R * x
    map_add' := fun x y => DistribSMul.smul_add R x y
    map_smul' := fun m x => mul_smul_comm m (↑R) x
    invFun := fun x ↦ R⁻¹ * x
    left_inv := by
      intro x
      simp
      rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
      simp
      exact ne_of_gt hR
    right_inv := by
      intro x
      simp
      rw [← mul_assoc, mul_inv_cancel₀, one_mul]
      simp
      exact ne_of_gt hR
    continuous_toFun := continuous_const_smul R
    continuous_invFun := continuous_const_smul R⁻¹
  }


  let F := f ∘ ℓ

  have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by
    apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R)
    exact h₁f
    intro x _
    apply ℓ.toContinuousLinearMap.analyticAt x

    intro x hx
    have : ℓ x = R * x := by rfl
    rw [this]
    simp
    simp at hx
    rw [abs_of_pos hR]
    calc R * Complex.abs x
    _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
    _ = R := by simp

  have h₂F : F 0 ≠ 0 := by
    dsimp [F]
    have : ℓ 0 = R * 0 := by rfl
    rw [this]
    simpa

  let A := jensen_case_R_eq_one F h₁F h₂F

  dsimp [F] at A
  have {x : ℂ} : ℓ x = R * x := by rfl
  repeat
    simp_rw [this] at A
  simp at A
  simp
  rw [A]
  simp_rw [← const_mul_circleMap_zero]
  simp

  let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by
    intro ⟨x, hx⟩
    have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by
      simp
      simp at hx
      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
      rw [← this]
      norm_num
      calc R * Complex.abs x
      _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
      _ = R := by simp
    exact ⟨R • x, hy⟩

  let e' : (Metric.closedBall (0 : ℂ) R) → (Metric.closedBall (0 : ℂ) 1) := by
    intro ⟨x, hx⟩
    have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ℂ) 1 := by
      simp
      simp at hx
      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
      rw [← this]
      norm_num
      calc R⁻¹ * Complex.abs x
      _ ≤ R⁻¹ * R := by
        apply mul_le_mul_of_nonneg_left hx
        apply inv_nonneg.mpr
        exact abs_eq_self.mp (id (Eq.symm this))
      _ = 1 := by
        apply inv_mul_cancel₀
        exact Ne.symm (ne_of_lt hR)
    exact ⟨R⁻¹ • x, hy⟩

  apply finsum_eq_of_bijective e


  apply Function.bijective_iff_has_inverse.mpr
  use e'
  constructor
  · apply Function.leftInverse_iff_comp.mpr
    funext x
    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
    conv =>
      left
      arg 1
      rw [← smul_assoc, smul_eq_mul]
      rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))]
      rw [one_smul]
  · apply Function.rightInverse_iff_comp.mpr
    funext x
    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
    conv =>
      left
      arg 1
      rw [← smul_assoc, smul_eq_mul]
      rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))]
      rw [one_smul]

  intro x
  simp
  by_cases hx : x = (0 : ℂ)
  rw [hx]
  simp

  rw [log_mul, log_mul, log_inv, log_inv]
  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
  rw [← this]
  simp
  left
  congr 1

  dsimp [AnalyticOnNhd.order]
  rw [← AnalyticAt.order_comp_CLE ℓ]

  --
  simpa
  --
  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
  rw [← this]
  apply inv_ne_zero
  exact Ne.symm (ne_of_lt hR)
  --
  exact Ne.symm (ne_of_lt hR)
  --
  simp
  constructor
  · assumption
  · exact Ne.symm (ne_of_lt hR)