Move unused files to junk
This commit is contained in:
Stefan Kebekus
449
Nevanlinna/junk/holomorphic_JensenFormula.lean
Normal file
449
Nevanlinna/junk/holomorphic_JensenFormula.lean
Normal file
@@ -0,0 +1,449 @@
|
||||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.analyticOnNhd_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 : AnalyticOnNhd ℂ 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⟩ := AnalyticOnNhdCompact.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 [AnalyticOnNhd.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 (AnalyticOnNhd.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 : AnalyticOnNhd ℂ 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 : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by
|
||||
apply AnalyticOnNhd.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 [AnalyticOnNhd.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)
|
||||
528
Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean
Normal file
528
Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean
Normal file
@@ -0,0 +1,528 @@
|
||||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.analyticOnNhd_zeroSet
|
||||
import Nevanlinna.harmonicAt_examples
|
||||
import Nevanlinna.harmonicAt_meanValue
|
||||
import Nevanlinna.specialFunctions_CircleIntegral_affine
|
||||
import Nevanlinna.stronglyMeromorphicOn
|
||||
import Nevanlinna.stronglyMeromorphicOn_eliminate
|
||||
import Nevanlinna.meromorphicOn_divisor
|
||||
|
||||
open Real
|
||||
|
||||
|
||||
|
||||
theorem jensen_case_R_eq_one'
|
||||
(f : ℂ → ℂ)
|
||||
(h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1))
|
||||
(h₂f : f 0 ≠ 0) :
|
||||
log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
|
||||
|
||||
have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by
|
||||
constructor
|
||||
· apply Metric.nonempty_closedBall.mpr (by simp)
|
||||
· exact (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, Metric.mem_closedBall_self (by simp)⟩
|
||||
|
||||
have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
|
||||
exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor
|
||||
|
||||
have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by
|
||||
intro x
|
||||
contrapose
|
||||
simp
|
||||
intro hx
|
||||
rw [hx]
|
||||
simp
|
||||
rw [finsum_eq_sum_of_support_subset _ h₄f]
|
||||
|
||||
obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f h'₂f
|
||||
|
||||
have h₁F : Function.mulSupport (fun u ↦ fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) ⊆ h₃f.toFinset := by
|
||||
intro u
|
||||
contrapose
|
||||
simp
|
||||
intro hu
|
||||
rw [hu]
|
||||
simp
|
||||
exact rfl
|
||||
rw [finprod_eq_prod_of_mulSupport_subset _ h₁F] at h₄F
|
||||
|
||||
let G := fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖
|
||||
|
||||
have h₁G {z : ℂ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) ⊆ h₃f.toFinset := by
|
||||
intro s
|
||||
contrapose
|
||||
simp
|
||||
intro hs
|
||||
rw [hs]
|
||||
simp
|
||||
|
||||
have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
|
||||
intro z h₁z h₂z
|
||||
|
||||
rw [h₄F]
|
||||
simp only [Pi.mul_apply, norm_mul]
|
||||
simp only [Finset.prod_apply, norm_prod, norm_zpow]
|
||||
rw [Real.log_mul]
|
||||
rw [Real.log_prod]
|
||||
simp_rw [Real.log_zpow]
|
||||
dsimp only [G]
|
||||
rw [finsum_eq_sum_of_support_subset _ h₁G]
|
||||
--
|
||||
intro x hx
|
||||
have : z ≠ x := by
|
||||
by_contra hCon
|
||||
rw [← hCon] at hx
|
||||
simp at hx
|
||||
rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
|
||||
unfold MeromorphicOn.divisor at hx
|
||||
simp [h₁z] at hx
|
||||
tauto
|
||||
apply zpow_ne_zero
|
||||
simpa
|
||||
-- Complex.abs (F z) ≠ 0
|
||||
simp
|
||||
exact h₃F ⟨z, h₁z⟩
|
||||
--
|
||||
rw [Finset.prod_ne_zero_iff]
|
||||
intro x hx
|
||||
have : z ≠ x := by
|
||||
by_contra hCon
|
||||
rw [← hCon] at hx
|
||||
simp at hx
|
||||
rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z
|
||||
unfold MeromorphicOn.divisor at hx
|
||||
simp [h₁z] at hx
|
||||
tauto
|
||||
apply zpow_ne_zero
|
||||
simpa
|
||||
|
||||
|
||||
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)⁻¹' (h₃f.toFinset) := by
|
||||
intro a ha
|
||||
simp at ha
|
||||
simp
|
||||
by_contra C
|
||||
have t₀ : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
|
||||
circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
|
||||
have t₁ : f (circleMap 0 1 a) ≠ 0 := by
|
||||
let A := h₁f (circleMap 0 1 a) t₀
|
||||
rw [← A.order_eq_zero_iff]
|
||||
unfold MeromorphicOn.divisor at C
|
||||
simp [t₀] at C
|
||||
rcases C with C₁|C₂
|
||||
· assumption
|
||||
· let B := h₁f.meromorphicOn.order_ne_top' h₁U
|
||||
let C := fun q ↦ B q ⟨(circleMap 0 1 a), t₀⟩
|
||||
rw [C₂] at C
|
||||
have : ∃ u : (Metric.closedBall (0 : ℂ) 1), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
|
||||
use ⟨(0 : ℂ), (by simp)⟩
|
||||
let H := h₁f 0 (by simp)
|
||||
let K := H.order_eq_zero_iff.2 h₂f
|
||||
rw [K]
|
||||
simp
|
||||
let D := C this
|
||||
tauto
|
||||
exact ha.2 (decompose_f (circleMap 0 1 a) t₀ t₁)
|
||||
|
||||
apply Set.Countable.mono t₀
|
||||
apply Set.Countable.preimage_circleMap
|
||||
apply Set.Finite.countable
|
||||
exact Finset.finite_toSet h₃f.toFinset
|
||||
--
|
||||
simp
|
||||
|
||||
|
||||
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, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
|
||||
dsimp [G]
|
||||
|
||||
rw [intervalIntegral.integral_add]
|
||||
congr
|
||||
have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) ⊆ h₃f.toFinset := by
|
||||
intro s hs
|
||||
simp at hs
|
||||
simp [hs.1]
|
||||
conv =>
|
||||
left
|
||||
arg 1
|
||||
intro x
|
||||
rw [finsum_eq_sum_of_support_subset _ t₀]
|
||||
rw [intervalIntegral.integral_finset_sum]
|
||||
let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))
|
||||
have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))) ⊆ h₃f.toFinset := by
|
||||
simp
|
||||
intro s
|
||||
contrapose!
|
||||
simp
|
||||
tauto
|
||||
conv =>
|
||||
right
|
||||
rw [finsum_eq_sum_of_support_subset _ t₁]
|
||||
simp
|
||||
|
||||
-- ∀ 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
|
||||
-- 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
|
||||
exact h₃F ⟨(circleMap 0 1 x), (by simp)⟩
|
||||
|
||||
-- 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 AnalyticAt.differentiableAt
|
||||
exact h₂F (circleMap 0 1 x) (by simp)
|
||||
-- ContinuousAt (fun x => circleMap 0 1 x) x
|
||||
apply Continuous.continuousAt
|
||||
apply continuous_circleMap
|
||||
-- IntervalIntegrable (fun x => ∑ᶠ (s : ℂ), ↑(↑⋯.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) MeasureTheory.volume 0 (2 * π)
|
||||
--simp? at h₁G
|
||||
have h₁G' {z : ℂ} : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * log (Complex.abs (z - s))) ⊆ ↑h₃f.toFinset := by
|
||||
exact h₁G
|
||||
conv =>
|
||||
arg 1
|
||||
intro z
|
||||
rw [finsum_eq_sum_of_support_subset _ h₁G']
|
||||
conv =>
|
||||
arg 1
|
||||
rw [← Finset.sum_fn]
|
||||
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
|
||||
-- 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
|
||||
exact AnalyticAt.holomorphicAt (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
|
||||
|
||||
|
||||
have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖) ⊆ ↑h₃f.toFinset := by
|
||||
intro s hs
|
||||
simp at hs
|
||||
simp [hs.1]
|
||||
rw [finsum_eq_sum_of_support_subset _ h₁G'] at decompose_int_G
|
||||
have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖ = 0 := by
|
||||
apply Finset.sum_eq_zero
|
||||
intro x hx
|
||||
rw [int₃ _]
|
||||
simp
|
||||
simp at hx
|
||||
let ZZ := h₁f.meromorphicOn.divisor.supportInU
|
||||
simp at ZZ
|
||||
let UU := ZZ x hx
|
||||
simpa
|
||||
rw [this] at decompose_int_G
|
||||
|
||||
|
||||
simp at decompose_int_G
|
||||
|
||||
rw [int_logAbs_f_eq_int_G]
|
||||
rw [decompose_int_G]
|
||||
let X := h₄F
|
||||
nth_rw 1 [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 [add_comm]
|
||||
--
|
||||
intro x hx
|
||||
simp at hx
|
||||
rw [zpow_ne_zero_iff]
|
||||
by_contra hCon
|
||||
simp at hCon
|
||||
rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f
|
||||
rw [hCon] at hx
|
||||
unfold MeromorphicOn.divisor at hx
|
||||
simp at hx
|
||||
rw [h₂f] at hx
|
||||
tauto
|
||||
assumption
|
||||
--
|
||||
simp
|
||||
|
||||
by_contra hCon
|
||||
nth_rw 1 [h₄F] at h₂f
|
||||
simp at h₂f
|
||||
tauto
|
||||
--
|
||||
rw [Finset.prod_ne_zero_iff]
|
||||
intro x hx
|
||||
simp at hx
|
||||
rw [zpow_ne_zero_iff]
|
||||
by_contra hCon
|
||||
simp at hCon
|
||||
rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f
|
||||
rw [hCon] at hx
|
||||
unfold MeromorphicOn.divisor at hx
|
||||
simp at hx
|
||||
rw [h₂f] at hx
|
||||
tauto
|
||||
assumption
|
||||
|
||||
|
||||
|
||||
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 : StronglyMeromorphicOn f (Metric.closedBall 0 R))
|
||||
(h₂f : f 0 ≠ 0) :
|
||||
log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (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 : StronglyMeromorphicOn F (Metric.closedBall 0 1) := by
|
||||
sorry
|
||||
/-
|
||||
apply AnalyticOnNhd.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 [AnalyticOnNhd.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)
|
||||
Reference in New Issue
Block a user