Compare commits
No commits in common. "dba4e2d9c4d1e4ca5155b7c79ba0c94759ed40ac" and "712be956d0b6f80ead6baef90356f4e4cbb6997f" have entirely different histories.
dba4e2d9c4
...
712be956d0
|
|
@ -1,449 +1,172 @@
|
||||||
import Mathlib.Analysis.Complex.CauchyIntegral
|
|
||||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
|
||||||
import Nevanlinna.analyticOn_zeroSet
|
import Nevanlinna.analyticOn_zeroSet
|
||||||
import Nevanlinna.harmonicAt_examples
|
import Nevanlinna.harmonicAt_examples
|
||||||
import Nevanlinna.harmonicAt_meanValue
|
import Nevanlinna.harmonicAt_meanValue
|
||||||
import Nevanlinna.specialFunctions_CircleIntegral_affine
|
import Nevanlinna.specialFunctions_CircleIntegral_affine
|
||||||
|
|
||||||
open Real
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
theorem jensen_case_R_eq_one
|
theorem jensen_case_R_eq_one
|
||||||
(f : ℂ → ℂ)
|
(f : ℂ → ℂ)
|
||||||
(h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1))
|
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||||||
(h₂f : f 0 ≠ 0) :
|
(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
|
(S : Finset ℕ)
|
||||||
|
(a : S → ℂ)
|
||||||
|
(ha : ∀ s, a s ∈ Metric.ball 0 1)
|
||||||
|
(F : ℂ → ℂ)
|
||||||
|
(h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z)
|
||||||
|
(h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, 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
|
||||||
|
|
||||||
have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
|
have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by sorry
|
||||||
(convex_closedBall (0 : ℂ) 1).isPreconnected
|
have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := by sorry
|
||||||
|
have h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1) := by sorry
|
||||||
|
have h₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by sorry
|
||||||
|
|
||||||
have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
|
let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
|
||||||
isCompact_closedBall 0 1
|
obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α
|
||||||
|
have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry
|
||||||
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‖
|
let logAbsF := fun w ↦ Real.log ‖F w‖
|
||||||
|
|
||||||
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
|
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
|
||||||
intro z hz
|
intro z hz
|
||||||
apply logabs_of_holomorphicAt_is_harmonic
|
apply logabs_of_holomorphicAt_is_harmonic
|
||||||
apply h'₁F z hz
|
apply h₁F z hz
|
||||||
exact h₂F z hz
|
exact h₂F z hz
|
||||||
|
|
||||||
|
have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
|
||||||
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
|
apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
|
||||||
|
|
||||||
simp_rw [← Complex.norm_eq_abs] at decompose_int_G
|
have t₂ : ∀ s, f (a s) = 0 := by
|
||||||
rw [t₁] at decompose_int_G
|
intro s
|
||||||
|
|
||||||
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]
|
rw [h₃F]
|
||||||
simp
|
simp
|
||||||
have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
|
right
|
||||||
calc π⁻¹ * 2⁻¹ * (2 * π * l)
|
apply Finset.prod_eq_zero_iff.2
|
||||||
_ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
|
use s
|
||||||
_ = π⁻¹ * π * 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
|
simp
|
||||||
|
|
||||||
rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
|
let logAbsf := fun w ↦ Real.log ‖f w‖
|
||||||
|
have s₀ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
|
||||||
|
intro z h₁z h₂z
|
||||||
|
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
|
simp
|
||||||
|
by_contra ha'
|
||||||
|
rw [ha'] at h₂z
|
||||||
|
exact h₂z (t₂ s)
|
||||||
|
-- Complex.abs (F z) ≠ 0
|
||||||
simp
|
simp
|
||||||
intro x ⟨h₁x, _⟩
|
exact h₂F z h₁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 h₂z
|
||||||
|
let A := t₂ s
|
||||||
|
exact h₂z A
|
||||||
|
|
||||||
|
have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
|
||||||
|
intro z h₁z h₂z
|
||||||
|
rw [s₀ z h₁z]
|
||||||
simp
|
simp
|
||||||
|
assumption
|
||||||
|
|
||||||
dsimp [AnalyticOn.order] at h₁x
|
have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
|
||||||
simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
|
rw [s₁ 0 this h₂f] at t₁
|
||||||
exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
|
|
||||||
|
|
||||||
--
|
have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
|
||||||
intro x hx
|
rw [h₃F]
|
||||||
simp at hx
|
|
||||||
simp
|
simp
|
||||||
intro h₁x
|
constructor
|
||||||
nth_rw 1 [← h₁x] at h₂f
|
· have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
|
||||||
tauto
|
exact h₂F (circleMap 0 1 x) this
|
||||||
|
· by_contra h'
|
||||||
--
|
obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h'
|
||||||
rw [Finset.prod_ne_zero_iff]
|
have : circleMap 0 1 x = a s := by
|
||||||
intro x hx
|
rw [← sub_zero (circleMap 0 1 x)]
|
||||||
simp at hx
|
nth_rw 2 [← h₂s]
|
||||||
simp
|
simp
|
||||||
intro h₁x
|
let A := ha s
|
||||||
nth_rw 1 [← h₁x] at h₂f
|
rw [← this] at A
|
||||||
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 at A
|
||||||
|
|
||||||
|
have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
|
||||||
|
simp_rw [s₁ (circleMap 0 1 _) this 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
|
simp
|
||||||
rw [A]
|
have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
|
||||||
simp_rw [← const_mul_circleMap_zero]
|
ring_nf
|
||||||
|
simp [mul_inv_cancel₀ Real.pi_ne_zero]
|
||||||
|
rw [this]
|
||||||
simp
|
simp
|
||||||
|
rfl
|
||||||
let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by
|
-- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
|
||||||
intro ⟨x, hx⟩
|
intro i _
|
||||||
have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by
|
apply Continuous.intervalIntegrable
|
||||||
simp
|
apply continuous_iff_continuousAt.2
|
||||||
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
|
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
|
simp
|
||||||
by_cases hx : x = (0 : ℂ)
|
by_contra ha'
|
||||||
rw [hx]
|
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
|
simp
|
||||||
|
exact h₀
|
||||||
rw [log_mul, log_mul, log_inv, log_inv]
|
apply ContinuousAt.comp
|
||||||
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
|
apply Complex.continuous_abs.continuousAt
|
||||||
rw [← this]
|
apply ContinuousAt.comp
|
||||||
|
apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
|
||||||
|
apply HolomorphicAt.contDiffAt
|
||||||
|
apply h₁f
|
||||||
simp
|
simp
|
||||||
left
|
let A := continuous_circleMap 0 1
|
||||||
congr 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)
|
||||||
dsimp [AnalyticOn.order]
|
apply Continuous.intervalIntegrable
|
||||||
rw [← AnalyticAt.order_comp_CLE ℓ]
|
apply continuous_finset_sum
|
||||||
|
intro i _
|
||||||
--
|
apply continuous_iff_continuousAt.2
|
||||||
simpa
|
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) :=
|
||||||
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
|
rfl
|
||||||
rw [← this]
|
rw [this]
|
||||||
apply inv_ne_zero
|
apply ContinuousAt.comp
|
||||||
exact Ne.symm (ne_of_lt hR)
|
apply Real.continuousAt_log
|
||||||
--
|
|
||||||
exact Ne.symm (ne_of_lt hR)
|
|
||||||
--
|
|
||||||
simp
|
simp
|
||||||
constructor
|
by_contra ha'
|
||||||
· assumption
|
let A := ha i
|
||||||
· exact Ne.symm (ne_of_lt hR)
|
rw [← ha'] at A
|
||||||
|
simp at A
|
||||||
|
apply ContinuousAt.comp
|
||||||
|
apply Complex.continuous_abs.continuousAt
|
||||||
|
fun_prop
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,449 @@
|
||||||
|
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)
|
||||||
Loading…
Reference in New Issue