working…
This commit is contained in:
Stefan Kebekus
parent
960af65b57
commit
567b08aa5b
|
|
@ -1,3 +1,4 @@
|
|||
import Nevanlinna.analyticOn_zeroSet
|
||||
import Nevanlinna.harmonicAt_examples
|
||||
import Nevanlinna.harmonicAt_meanValue
|
||||
import Nevanlinna.specialFunctions_CircleIntegral_affine
|
||||
|
|
@ -16,6 +17,17 @@ theorem jensen_case_R_eq_one
|
|||
(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) := 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‖
|
||||
|
||||
have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
|
||||
|
|
|
|||
|
|
@ -1,41 +1,163 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.analyticOn_zeroSet
|
||||
import Nevanlinna.harmonicAt_examples
|
||||
import Nevanlinna.harmonicAt_meanValue
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
|
||||
open Real
|
||||
|
||||
|
||||
lemma xx
|
||||
def ZeroFinset
|
||||
{f : ℂ → ℂ}
|
||||
{S : Set ℂ}
|
||||
(h₁S : IsPreconnected S)
|
||||
(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
|
||||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) :
|
||||
Finset ℂ := by
|
||||
|
||||
let o : ℂ → ℕ := by
|
||||
intro z
|
||||
if hz : z ∈ S then
|
||||
let A := hf z hz
|
||||
let B := A.order
|
||||
let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
|
||||
have hZ : Set.Finite Z := by sorry
|
||||
exact hZ.toFinset
|
||||
|
||||
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
|
||||
|
||||
|
||||
theorem jensen_case_R_eq_one'
|
||||
theorem jensen_case_R_eq_one
|
||||
(f : ℂ → ℂ)
|
||||
(h₁f : Differentiable ℂ f)
|
||||
(h₂f : f 0 ≠ 0)
|
||||
(S : Finset ℕ)
|
||||
(a : S → ℂ)
|
||||
(ha : ∀ s, a s ∈ Metric.ball 0 1)
|
||||
(F : ℂ → ℂ)
|
||||
(h₁F : Differentiable ℂ F)
|
||||
(h₂F : ∀ z, 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
|
||||
(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, 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, (z - s) ^ (order s) := by sorry
|
||||
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue