279 lines
8.6 KiB
Plaintext
279 lines
8.6 KiB
Plaintext
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
|
||
|
||
|
||
noncomputable def ZeroFinset
|
||
{f : ℂ → ℂ}
|
||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||
(h₂f : f 0 ≠ 0) :
|
||
Finset ℂ := by
|
||
|
||
let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
|
||
have hZ : Set.Finite Z := by
|
||
dsimp [Z]
|
||
rw [Set.inter_comm]
|
||
apply finiteZeros
|
||
-- Ball is preconnected
|
||
apply IsConnected.isPreconnected
|
||
apply Convex.isConnected
|
||
exact convex_closedBall 0 1
|
||
exact Set.nonempty_of_nonempty_subtype
|
||
--
|
||
exact isCompact_closedBall 0 1
|
||
--
|
||
intro x hx
|
||
have A := (h₁f x hx)
|
||
let B := HolomorphicAt_iff.1 A
|
||
obtain ⟨s, h₁s, h₂s, h₃s⟩ := B
|
||
apply DifferentiableOn.analyticAt (s := s)
|
||
intro z hz
|
||
apply DifferentiableAt.differentiableWithinAt
|
||
apply h₃s
|
||
exact hz
|
||
exact IsOpen.mem_nhds h₁s h₂s
|
||
--
|
||
use 0
|
||
constructor
|
||
· simp
|
||
· exact h₂f
|
||
exact hZ.toFinset
|
||
|
||
|
||
lemma ZeroFinset_mem_iff
|
||
{f : ℂ → ℂ}
|
||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||
{h₂f : f 0 ≠ 0}
|
||
(z : ℂ) :
|
||
z ∈ ↑(ZeroFinset h₁f h₂f) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
|
||
dsimp [ZeroFinset]; simp
|
||
tauto
|
||
|
||
|
||
noncomputable def order
|
||
{f : ℂ → ℂ}
|
||
{h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z}
|
||
{h₂f : f 0 ≠ 0} :
|
||
ZeroFinset h₁f h₂f → ℕ := by
|
||
intro i
|
||
let A := ((ZeroFinset_mem_iff h₁f i).1 i.2).1
|
||
let B := (h₁f i.1 A).analyticAt
|
||
exact B.order.toNat
|
||
|
||
|
||
|
||
theorem jensen_case_R_eq_one
|
||
(f : ℂ → ℂ)
|
||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||
(h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
|
||
(h₂f : f 0 ≠ 0) :
|
||
log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
|
||
|
||
have F : ℂ → ℂ := by sorry
|
||
have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
|
||
have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
|
||
have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry
|
||
|
||
let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f 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 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 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 * π)
|
||
intro i hi
|
||
apply IntervalIntegrable.const_mul
|
||
have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
|
||
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
|
||
-- 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]
|
||
--
|
||
apply ContinuousAt.comp
|
||
apply Complex.continuous_abs.continuousAt
|
||
apply ContinuousAt.comp
|
||
apply DifferentiableAt.continuousAt (𝕜 := ℂ )
|
||
apply HolomorphicAt.differentiableAt
|
||
simp [h₁F]
|
||
--
|
||
apply Continuous.continuousAt
|
||
apply continuous_circleMap
|
||
--
|
||
have : (fun x => ∑ s ∈ (ZeroFinset h₁f h₂f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
|
||
= ∑ s ∈ (ZeroFinset h₁f h₂f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
|
||
funext x
|
||
simp
|
||
rw [this]
|
||
apply IntervalIntegrable.sum
|
||
intro i h₂i
|
||
apply IntervalIntegrable.const_mul
|
||
have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
|
||
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 this
|
||
rw [t₁] at this
|
||
|
||
|
||
|
||
|
||
sorry
|