working
This commit is contained in:
parent
6651c0852a
commit
47e1bfe35e
@ -16,7 +16,6 @@ lemma h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
|
||||
|
||||
theorem jensen_case_R_eq_one
|
||||
(f : ℂ → ℂ)
|
||||
(h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
|
||||
(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
|
||||
@ -116,10 +115,6 @@ theorem jensen_case_R_eq_one
|
||||
exact Ne.symm (zero_ne_one' ℝ)
|
||||
|
||||
|
||||
have h₁Gi : ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, 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 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
|
||||
@ -131,7 +126,7 @@ theorem jensen_case_R_eq_one
|
||||
-- ∀ 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 hi
|
||||
intro i _
|
||||
apply IntervalIntegrable.const_mul
|
||||
--simp at this
|
||||
by_cases h₂i : ‖i.1‖ = 1
|
||||
@ -186,7 +181,7 @@ theorem jensen_case_R_eq_one
|
||||
simp
|
||||
rw [this]
|
||||
apply IntervalIntegrable.sum
|
||||
intro i h₂i
|
||||
intro i _
|
||||
apply IntervalIntegrable.const_mul
|
||||
--have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
|
||||
--simp at this
|
||||
@ -260,7 +255,7 @@ theorem jensen_case_R_eq_one
|
||||
rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset)]
|
||||
simp
|
||||
simp
|
||||
intro x ⟨h₁x, h₂x⟩
|
||||
intro x ⟨h₁x, _⟩
|
||||
simp
|
||||
|
||||
dsimp [AnalyticOn.order] at h₁x
|
||||
|
@ -8,10 +8,6 @@ import Nevanlinna.periodic_integrability
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
-- Integrability of periodic functions
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- Lemmas for the circleMap
|
||||
@ -46,6 +42,20 @@ lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x))
|
||||
|
||||
-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
|
||||
|
||||
lemma int'₀
|
||||
{a : ℂ}
|
||||
(ha : a ∈ Metric.ball 0 1) :
|
||||
IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
|
||||
apply Continuous.intervalIntegrable
|
||||
apply Continuous.log
|
||||
fun_prop
|
||||
simp
|
||||
intro x
|
||||
by_contra h₁a
|
||||
rw [← h₁a] at ha
|
||||
simp at ha
|
||||
|
||||
|
||||
lemma int₀
|
||||
{a : ℂ}
|
||||
(ha : a ∈ Metric.ball 0 1) :
|
||||
@ -210,7 +220,6 @@ lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary
|
||||
rw [zero_add]
|
||||
exact int'₁
|
||||
|
||||
|
||||
lemma int₁ :
|
||||
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user