nevanlinna/Nevanlinna/holomorphic_JensenFormula2....

450 lines
12 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 Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.analyticOn_zeroSet
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
import Nevanlinna.specialFunctions_CircleIntegral_affine
open Real
theorem jensen_case_R_eq_one
(f : )
(h₁f : AnalyticOn f (Metric.closedBall 0 1))
(h₂f : f 0 ≠ 0) :
log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
have h₁U : IsPreconnected (Metric.closedBall (0 : ) 1) :=
(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; simp; exact h₂f
obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
have h'₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z := by
intro z h₁z
apply AnalyticAt.holomorphicAt
exact h₁F z h₁z
let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
intro z h₁z h₂z
conv =>
left
arg 1
rw [h₃F]
rw [smul_eq_mul]
rw [norm_mul]
rw [norm_prod]
left
arg 2
intro b
rw [norm_pow]
simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
rw [Real.log_mul]
rw [Real.log_prod]
conv =>
left
left
arg 2
intro s
rw [Real.log_pow]
dsimp [G]
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 [AnalyticOn.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 (AnalyticOn.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 : AnalyticOn 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 : AnalyticOn F (Metric.closedBall 0 1) := by
apply AnalyticOn.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 [AnalyticOn.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)