Compare commits

..

2 Commits

Author SHA1 Message Date
Stefan Kebekus 567b08aa5b working… 2024-08-21 17:04:45 +02:00
Stefan Kebekus 960af65b57 Update holomorphic_JensenFormula.lean 2024-08-21 10:12:36 +02:00
2 changed files with 191 additions and 54 deletions

View File

@ -1,3 +1,4 @@
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
@ -5,31 +6,38 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
theorem jensen_case_R_eq_one theorem jensen_case_R_eq_one
(f : ) (f : )
(h₁f : Differentiable f) (h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(h₂f : f 0 ≠ 0) (h₂f : f 0 ≠ 0)
(S : Finset ) (S : Finset )
(a : S → ) (a : S → )
(ha : ∀ s, a s ∈ Metric.ball 0 1) (ha : ∀ s, a s ∈ Metric.ball 0 1)
(F : ) (F : )
(h₁F : Differentiable F) (h₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z)
(h₂F : ∀ z, F z ≠ 0) (h₂F : ∀ z ∈ Metric.closedBall (0 : ) 1, F z ≠ 0)
(h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) (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 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) := by sorry
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
let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α
have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry
let logAbsF := fun w ↦ Real.log ‖F w‖ let logAbsF := fun w ↦ Real.log ‖F w‖
have t₀ : ∀ z ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
intro z _ intro z hz
apply logabs_of_holomorphicAt_is_harmonic apply logabs_of_holomorphicAt_is_harmonic
apply h₁F.holomorphicAt apply h₁F z hz
exact h₂F z exact h₂F z hz
have t₁ : (∫ (x : ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by 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 apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
have hρ : (1 : ) < (2 : ) := by linarith
apply harmonic_meanValue 2 1 hR hρ t₀
have t₂ : ∀ s, f (a s) = 0 := by have t₂ : ∀ s, f (a s) = 0 := by
intro s intro s
@ -41,8 +49,8 @@ theorem jensen_case_R_eq_one
simp simp
let logAbsf := fun w ↦ Real.log ‖f w‖ 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 have s₀ : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
intro z hz intro z h₁z h₂z
dsimp [logAbsf] dsimp [logAbsf]
rw [h₃F] rw [h₃F]
simp_rw [Complex.abs.map_mul] simp_rw [Complex.abs.map_mul]
@ -53,31 +61,34 @@ theorem jensen_case_R_eq_one
intro s hs intro s hs
simp simp
by_contra ha' by_contra ha'
rw [ha'] at hz rw [ha'] at hz
exact hz (t₂ s) exact hz (t₂ s)
-- Complex.abs (F z) ≠ 0 -- Complex.abs (F z) ≠ 0
simp simp
exact h₂F z exact h₂F z h₁z
-- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0 -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
by_contra h' by_contra h'
obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h' obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
simp at h'' simp at h''
rw [h''] at hz rw [h''] at hz
let A := t₂ s let A := t₂ s
exact hz A exact hz A
have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by have s₁ : ∀ z ∈ Metric.closedBall (0 : ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
intro z hz intro z h₁z h₂z
rw [s₀ z hz] rw [s₀ z hz]
simp simp
assumption
rw [s₁ 0 h₂f] at t₁ have : 0 ∈ Metric.closedBall (0 : ) 1 := by simp
rw [s₁ 0 this h₂f] at t₁
have h₀ {x : } : f (circleMap 0 1 x) ≠ 0 := by have h₀ {x : } : f (circleMap 0 1 x) ≠ 0 := by
rw [h₃F] rw [h₃F]
simp simp
constructor constructor
· exact h₂F (circleMap 0 1 x) · have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ) 1 := by simp
exact h₂F (circleMap 0 1 x) this
· by_contra h' · by_contra h'
obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h' obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h'
have : circleMap 0 1 x = a s := by have : circleMap 0 1 x = a s := by
@ -88,7 +99,8 @@ theorem jensen_case_R_eq_one
rw [← this] at A rw [← this] at A
simp at A simp at A
simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁ 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_sub] at t₁
rw [intervalIntegral.integral_finset_sum] at t₁ rw [intervalIntegral.integral_finset_sum] at t₁
@ -133,7 +145,10 @@ theorem jensen_case_R_eq_one
apply ContinuousAt.comp apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt apply Complex.continuous_abs.continuousAt
apply ContinuousAt.comp apply ContinuousAt.comp
apply h₁f.continuous.continuousAt apply ContDiffAt.continuousAt (f := f) (𝕜 := ) (n := 1)
apply HolomorphicAt.contDiffAt
apply h₁f
simp
let A := continuous_circleMap 0 1 let A := continuous_circleMap 0 1
apply A.continuousAt apply A.continuousAt
-- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi) -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)

View File

@ -1,41 +1,163 @@
import Mathlib.Analysis.Complex.CauchyIntegral import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.analyticOn_zeroSet
import Nevanlinna.harmonicAt_examples import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue import Nevanlinna.harmonicAt_meanValue
import Mathlib.Analysis.Analytic.IsolatedZeros
open Real
lemma xx def ZeroFinset
{f : } {f : }
{S : Set } (h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z) :
(h₁S : IsPreconnected S) Finset := by
(h₂S : IsCompact S)
(hf : ∀ s ∈ S, AnalyticAt f s) :
∃ o : , ∃ F : , ∀ z ∈ S, (AnalyticAt F z) ∧ (F z ≠ 0) ∧ (f z = F z * ∏ᶠ s ∈ S, (z - s) ^ (o s)) := by
let o : := by let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ) 1
intro z have hZ : Set.Finite Z := by sorry
if hz : z ∈ S then exact hZ.toFinset
let A := hf z hz
let B := A.order
exact (A.order : )
else
exact 0
def order
{f : }
{hf : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z} :
ZeroFinset hf → := by sorry
lemma ZeroFinset_mem_iff
{f : }
(hf : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(z : ) :
z ∈ ↑(ZeroFinset hf) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
sorry sorry
theorem jensen_case_R_eq_one' theorem jensen_case_R_eq_one
(f : ) (f : )
(h₁f : Differentiable f) (h₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt f z)
(h₂f : f 0 ≠ 0) (h'₁f : ∀ z ∈ Metric.closedBall (0 : ) 1, AnalyticAt f z)
(S : Finset ) (h₂f : f 0 ≠ 0) :
(a : S → ) log ‖f 0‖ = -∑ s : ZeroFinset h₁f, order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
(ha : ∀ s, a s ∈ Metric.ball 0 1)
(F : ) have F : := by sorry
(h₁F : Differentiable F) have h₁F : ∀ z ∈ Metric.closedBall (0 : ) 1, HolomorphicAt F z := by sorry
(h₂F : ∀ z, F z ≠ 0) have h₂F : ∀ z ∈ Metric.closedBall (0 : ) 1, F z ≠ 0 := by sorry
(h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f, (z - s) ^ (order s) := by sorry
:
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 G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f, (order s) * 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 [norm_mul]
rw [norm_prod]
right
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
right
arg 2
intro s
rw [Real.log_pow]
dsimp [G]
-- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
simp
intro s hs
rw [ZeroFinset_mem_iff h₁f s] at hs
rw [← hs.2] at h₂z
tauto
-- Complex.abs (F z) ≠ 0
simp
exact h₂F z h₁z
-- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
by_contra C
obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C
simp at h₂s
rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z
tauto
have : ∫ (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 := by
sorry
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
apply finiteZeros
-- IsPreconnected (Metric.closedBall (0 : ) 1)
apply IsConnected.isPreconnected
apply Convex.isConnected
exact convex_closedBall 0 1
exact Set.nonempty_of_nonempty_subtype
--
exact isCompact_closedBall 0 1
--
exact h'₁f
use 0
exact ⟨Metric.mem_closedBall_self (zero_le_one' ), h₂f⟩
exact Ne.symm (zero_ne_one' )
have h₁Gi : ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
-- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
sorry
have : ∫ (x : ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f).attach, ↑(order x) * ∫ (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 ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) *
-- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
-- This won't work, because the function **is not** continuous. Need to fix.
intro i hi
apply IntervalIntegrable.const_mul
exact h₁Gi i hi
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'
let A := ha i
rw [← ha'] at A
simp at A
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
fun_prop
sorry
sorry sorry