nevanlinna/Nevanlinna/specialFunctions_CircleIntegral_affine.lean

import Mathlib.MeasureTheory.Integral.Periodic
import Mathlib.MeasureTheory.Integral.CircleIntegral
import Nevanlinna.specialFunctions_Integral_log_sin
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
import Nevanlinna.periodic_integrability

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

-- Integrability of periodic functions





-- Lemmas for the circleMap

lemma l₀ {x₁ x₂ : ℝ} : (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
  dsimp [circleMap]
  simp
  rw [add_mul, Complex.exp_add]

lemma l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
  rw [Complex.norm_eq_abs, abs_circleMap_zero]
  simp

lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
  calc ‖(circleMap 0 1 x) - a‖
  _ = 1 * ‖(circleMap 0 1 x) - a‖ := by
    exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
  _ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
    rw [l₁]
  _ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
    exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
  _ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
    rw [mul_sub]
  _ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
    rw [l₀]
    simp
  _ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
    congr
    dsimp [circleMap]
    simp


-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.

lemma int₀
  {a : ℂ}
  (ha : a ∈ Metric.ball 0 1) :
  ∫ (x : ℝ) in (0)..2 * π, log ‖circleMap 0 1 x - a‖ = 0 := by

  by_cases h₁a : a = 0
  · -- case: a = 0
    rw [h₁a]
    simp

  -- case: a ≠ 0
  simp_rw [l₂]
  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
  conv =>
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]

  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
    dsimp [f₁]
    congr 4
    let A := periodic_circleMap 0 1 x
    simp at A
    exact id (Eq.symm A)
  conv =>
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
  simp
  dsimp [f₁]

  let ρ := ‖a‖⁻¹
  have hρ : 1 < ρ := by
    apply one_lt_inv_iff.mpr
    constructor
    · exact norm_pos_iff'.mpr h₁a
    · exact mem_ball_zero_iff.mp ha

  let F := fun z ↦ log ‖1 - z * a‖

  have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
    intro x hx
    apply logabs_of_holomorphicAt_is_harmonic
    apply Differentiable.holomorphicAt
    fun_prop
    apply sub_ne_zero_of_ne
    by_contra h
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
      _ < ρ * ‖a‖ := by
        apply (mul_lt_mul_right _).2
        exact mem_ball_zero_iff.mp hx
        exact norm_pos_iff'.mpr h₁a
      _ = 1 := by
        dsimp [ρ]
        apply inv_mul_cancel₀
        exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
    rw [← h] at this
    simp at this

  let A := harmonic_meanValue ρ 1 zero_lt_one hρ hf
  dsimp [F] at A
  simp at A
  exact A


-- Integral of log ‖circleMap 0 1 x - 1‖

lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by

  have t₁ {x : ℝ} : x ∈ Set.Ioo 0 π → log (4 * sin x ^ 2) = log 4 + 2 * log (sin x) := by
    intro hx
    rw [log_mul, log_pow]
    rfl
    exact Ne.symm (NeZero.ne' 4)
    apply pow_ne_zero 2
    apply (fun a => Ne.symm (ne_of_lt a))
    exact sin_pos_of_mem_Ioo hx


  have t₂ : Set.EqOn (fun y ↦ log (4 * sin y ^ 2)) (fun y ↦ log 4 + 2 * log (sin y)) (Set.Ioo 0 π) := by
    intro x hx
    simp
    rw [t₁ hx]

  rw [intervalIntegral.integral_congr_volume pi_pos t₂]
  rw [intervalIntegral.integral_add]
  rw [intervalIntegral.integral_const_mul]
  simp
  rw [integral_log_sin₂]
  have : (4 : ℝ) = 2 * 2 := by norm_num
  rw [this, log_mul]
  ring
  norm_num
  norm_num
  -- IntervalIntegrable (fun x => log 4) volume 0 π
  simp
  -- IntervalIntegrable (fun x => 2 * log (sin x)) volume 0 π
  apply IntervalIntegrable.const_mul
  exact intervalIntegrable_log_sin

lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2 := by
  dsimp [Complex.abs]
  rw [log_sqrt (Complex.normSq_nonneg (circleMap 0 1 x - 1))]
  congr
  calc Complex.normSq (circleMap 0 1 x - 1)
  _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
    dsimp [circleMap]
    rw [Complex.normSq_apply]
    simp
  _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
    ring
  _ = 2 - 2 * cos x := by
    rw [sin_sq_add_cos_sq]
    norm_num
  _ = 2 - 2 * cos (2 * (x / 2)) := by
    rw [← mul_div_assoc]
    congr; norm_num
  _ = 4 - 4 * cos (x / 2) ^ 2 := by
    rw [cos_two_mul]
    ring
  _ = 4 * sin (x / 2) ^ 2 := by
    nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
    ring

lemma int'₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖
  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume 0 (2 * π) := by

  simp_rw [logAffineHelper]
  apply IntervalIntegrable.div_const
  rw [← IntervalIntegrable.comp_mul_left_iff (c := 2) (Ne.symm (NeZero.ne' 2))]
  simp

  have h₁ : Set.EqOn (fun x => log (4 * sin x ^ 2)) (fun x => log 4 + 2 * log (sin x)) (Set.Ioo 0 π) := by
    intro x hx
    simp [log_mul (Ne.symm (NeZero.ne' 4)), log_pow, ne_of_gt (sin_pos_of_mem_Ioo hx)]
  rw [IntervalIntegrable.integral_congr_Ioo pi_nonneg h₁]
  apply IntervalIntegrable.add
  simp
  apply IntervalIntegrable.const_mul
  exact intervalIntegrable_log_sin

lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary intervals
  ∀ (t₁ t₂ : ℝ), IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume t₁ t₂ := by
  intro t₁ t₂

  apply periodic_integrability4 (T := 2 * π) (t := 0)
  --
  have : (fun x => log ‖circleMap 0 1 x - 1‖) = (fun x => log ‖x - 1‖) ∘ (circleMap 0 1) := rfl
  rw [this]
  apply Function.Periodic.comp
  exact periodic_circleMap 0 1
  --
  exact two_pi_pos
  --
  rw [zero_add]
  exact int'₁


lemma int₁ :
  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by

  simp_rw [logAffineHelper]
  simp

  have : ∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2) =  2 * ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) := by
    have : 1 = 2 * (2 : ℝ)⁻¹ := by exact Eq.symm (mul_inv_cancel_of_invertible 2)
    nth_rw 1 [← one_mul (∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2))]
    rw [← mul_inv_cancel_of_invertible 2, mul_assoc]
    let f := fun y ↦ log (4 * sin y ^ 2)
    have {x : ℝ} : log (4 * sin (x / 2) ^ 2) = f (x / 2) := by simp
    conv =>
      left
      right
      right
      arg 1
      intro x
      rw [this]
    rw [intervalIntegral.inv_mul_integral_comp_div 2]
    simp
  rw [this]
  simp
  exact int₁₁


-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ = 1

lemma int'₂
  {a : ℂ}
  (ha : ‖a‖ = 1) :
  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by

  simp_rw [l₂]
  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
  conv =>
    arg 1
    intro x
    rw [this]
  rw [IntervalIntegrable.iff_comp_neg]

  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
    dsimp [f₁]
    congr 4
    let A := periodic_circleMap 0 1 x
    simp at A
    exact id (Eq.symm A)
  conv =>
    arg 1
    intro x
    arg 0
    intro w
    rw [this]
  simp
  have : 0 = 2 * π - 2 * π := by ring
  rw [this]
  have : -(2 * π ) = 0 - 2 * π := by ring
  rw [this]
  apply IntervalIntegrable.comp_add_right _ (2 * π) --f₁ (2 * π)
  dsimp [f₁]

  have : ∃ ζ, a = circleMap 0 1 ζ := by
    apply Set.exists_range_iff.mp
    use a
    simp
    exact ha
  obtain ⟨ζ, hζ⟩ := this
  rw [hζ]
  simp_rw [l₀]

  have : 2 * π  = (2 * π + ζ) - ζ := by ring
  rw [this]
  have : 0 = ζ - ζ := by ring
  rw [this]
  have : (fun w => log (Complex.abs (1 - circleMap 0 1 (w + ζ)))) = fun x ↦ (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w)))) (x + ζ) := rfl
  rw [this]
  apply IntervalIntegrable.comp_add_right (f := (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w))))) _ ζ

  have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
    have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
    rw [this]
    apply Function.Periodic.comp
    exact periodic_circleMap 0 1

  let A := int''₁ (2 * π + ζ) ζ
  have {x : ℝ} : ‖circleMap 0 1 x - 1‖ = Complex.abs (1 - circleMap 0 1 x) := AbsoluteValue.map_sub Complex.abs (circleMap 0 1 x) 1
  simp_rw [this] at A
  exact A


lemma int₂
  {a : ℂ}
  (ha : ‖a‖ = 1) :
  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by

  simp_rw [l₂]
  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
  conv =>
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]

  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
    dsimp [f₁]
    congr 4
    let A := periodic_circleMap 0 1 x
    simp at A
    exact id (Eq.symm A)
  conv =>
    left
    arg 1
    intro x
    rw [this]
  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
  simp
  dsimp [f₁]

  have : ∃ ζ, a = circleMap 0 1 ζ := by
    apply Set.exists_range_iff.mp
    use a
    simp
    exact ha
  obtain ⟨ζ, hζ⟩ := this
  rw [hζ]
  simp_rw [l₀]

  rw [intervalIntegral.integral_comp_add_right (f := fun x ↦ log (Complex.abs (1 - circleMap 0 1 (x))))]

  have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
    have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
    rw [this]
    apply Function.Periodic.comp
    exact periodic_circleMap 0 1

  let A := Function.Periodic.intervalIntegral_add_eq this ζ 0
  simp at A
  simp
  rw [add_comm]
  rw [A]

  have {x : ℝ} : log (Complex.abs (1 - circleMap 0 1 x)) = log ‖circleMap 0 1 x - 1‖ := by
    rw [← AbsoluteValue.map_neg Complex.abs]
    simp
  simp_rw [this]
  exact int₁