nevanlinna/Nevanlinna/holomorphic_JensenFormula.lean

262 lines
7.4 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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
lemma int₁ :
∫ (x : ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - 1‖ = 0 := by
dsimp [circleMap]
sorry
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