266 lines
7.6 KiB
Plaintext
266 lines
7.6 KiB
Plaintext
import Mathlib.MeasureTheory.Integral.Periodic
|
||
import Mathlib.MeasureTheory.Integral.CircleIntegral
|
||
import Nevanlinna.specialFunctions_Integral_log_sin
|
||
import Nevanlinna.harmonicAt_examples
|
||
import Nevanlinna.harmonicAt_meanValue
|
||
|
||
open scoped Interval Topology
|
||
open Real Filter MeasureTheory intervalIntegral
|
||
|
||
|
||
|
||
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 : ℝ} : 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
|
||
|
||
|
||
-- 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 * Real.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]
|
||
rw [← IntervalIntegrable.comp_mul_left_iff (c := 2) (Ne.symm (NeZero.ne' 2))]
|
||
simp
|
||
|
||
sorry
|
||
|
||
|
||
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₁₁
|
||
|
||
|
||
lemma int₂
|
||
{a : ℂ}
|
||
(ha : ‖a‖ = 1) :
|
||
∫ x in (0)..(2 * Real.pi), log ‖circleMap 0 1 x - a‖ = 0 := by
|
||
|
||
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₁]
|
||
|
||
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₁
|