nevanlinna/Nevanlinna/holomorphic_JensenFormula.lean

import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue

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

lemma int₀
  {a : ℂ}
  (ha : a ∈ Metric.ball 0 1) :
  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.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 : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.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 ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]

  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := 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 * Real.pi)]
  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 ↦ Real.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 Real.zero_lt_one hρ hf
  dsimp [F] at A
  simp at A
  exact A


theorem jensen_case_R_eq_one
  (f : ℂ → ℂ)
  (h₁f : Differentiable ℂ f)
  (h₂f : f 0 ≠ 0)
  (S : Finset ℕ)
  (a : S → ℂ)
  (ha : ∀ s, a s ∈ Metric.ball 0 1)
  (F : ℂ → ℂ)
  (h₁F : Differentiable ℂ F)
  (h₂F : ∀ z, F z ≠ 0)
  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s))
  :
  Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by

  let logAbsF := fun w ↦ Real.log ‖F w‖

  have t₀ : ∀ z ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by
    intro z _
    apply logabs_of_holomorphicAt_is_harmonic
    apply h₁F.holomorphicAt
    exact h₂F z

  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
    have hR : (0 : ℝ) < (1 : ℝ) := by apply Real.zero_lt_one
    have hρ : (1 : ℝ) < (2 : ℝ) := by linarith
    apply harmonic_meanValue 2 1 hR hρ t₀


  have t₂ : ∀ s, f (a s) = 0 := by
    intro s
    rw [h₃F]
    simp
    right
    apply Finset.prod_eq_zero_iff.2
    use s
    simp

  let logAbsf := fun w ↦ Real.log ‖f w‖
  have s₀ : ∀ z, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
    intro z hz
    dsimp [logAbsf]
    rw [h₃F]
    simp_rw [Complex.abs.map_mul]
    rw [Complex.abs_prod]
    rw [Real.log_mul]
    rw [Real.log_prod]
    rfl
    intro s hs
    simp
    by_contra ha'
    rw [ha'] at hz
    exact hz (t₂ s)
    -- Complex.abs (F z) ≠ 0
    simp
    exact h₂F z
    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
    by_contra h'
    obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
    simp at h''
    rw [h''] at hz
    let A := t₂ s
    exact hz A

  have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
    intro z hz
    rw [s₀ z hz]
    simp

  rw [s₁ 0 h₂f] at t₁

  have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
    rw [h₃F]
    simp
    constructor
    · exact h₂F (circleMap 0 1 x)
    · by_contra h'
      obtain ⟨s, _, h₂s⟩  := Finset.prod_eq_zero_iff.1 h'
      have : circleMap 0 1 x = a s := by
        rw [← sub_zero (circleMap 0 1 x)]
        nth_rw 2 [← h₂s]
        simp
      let A := ha s
      rw [← this] at A
      simp at A

  simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
  rw [intervalIntegral.integral_sub] at t₁
  rw [intervalIntegral.integral_finset_sum] at t₁

  simp_rw [int₀ (ha _)] at t₁
  simp at t₁
  rw [t₁]
  simp
  have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
    ring_nf
    simp [mul_inv_cancel Real.pi_ne_zero]
  rw [this]
  simp
  rfl
  -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
  intro i _
  apply Continuous.intervalIntegrable
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  apply Real.continuousAt_log
  simp
  by_contra ha'
  let A := ha i
  rw [← ha'] at A
  simp at A
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  fun_prop
  -- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
  apply Continuous.intervalIntegrable
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  simp
  exact h₀
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  apply ContinuousAt.comp
  apply h₁f.continuous.continuousAt
  let A := continuous_circleMap 0 1
  apply A.continuousAt
  -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
  apply Continuous.intervalIntegrable
  apply continuous_finset_sum
  intro i _
  apply continuous_iff_continuousAt.2
  intro x
  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
    rfl
  rw [this]
  apply ContinuousAt.comp
  apply Real.continuousAt_log
  simp
  by_contra ha'
  let A := ha i
  rw [← ha'] at A
  simp at A
  apply ContinuousAt.comp
  apply Complex.continuous_abs.continuousAt
  fun_prop