Documentation

LeanPool.LeanComplexAnalysis.Harmonic.Positive.HerglotzRieszRepresentations

The Herglotz–Riesz Representation Theorem #

This file proves the Herglotz–Riesz representation theorem for positive harmonic functions on the unit disc, as well as for analytic functions with positive real part on the unit disc.

Main Results #

Theorem HerglotzRiesz_representation_harmonic: Every harmonic function u : ℂ → ℝ on the unit disc with u(0) = 1 and u(z) > 0 for all z in the unit disc can be represented as

u z = ∫ (1 - ‖z‖^2) / ‖x - z‖^2 dμ(x)

where μ is a uniquely determined probability measure supported on the unit circle.

We also prove the analytic version, Theorem HerglotzRiesz_representation_analytic: Every analytic function p on the unit disc with p(0) = 1 and mapping the unit disc into the right half-plane can be represented as

  p(z) = ∫ (x + z)/(x - z) dμ(x)

where μ is a uniquely determined probability measure supported on the unit circle.

Implementation Notes #

The proof proceeds by:

The existence of μ is proven in HerglotzRiesz_representation_existence. The construction uses the Banach-Alaoglu theorem and the Riesz-Markov-Kakutani representation theorem. Furthermore, we use the Poisson integral formula poisson_formula_of_harmonicOn_scaled_unitDisc.
Uniqueness of μ is established via the identity principle in Theorem HerglotzRiesz_representation_uniqueness.
Finally, we combine the two parts to obtain HerglotzRiesz_representation_analytic and derive the harmonic version HerglotzRiesz_representation_harmonic.

References #

G. Herglotz, "Über Potenzreihen mit positivem, reellen Teil im Einheitskreis", 1911, Ber. Sächs. Ges. Wiss. Leipzig, 63, 501–511.
F. Riesz, "Sur certains systèmes singuliers d'équations intégrales", 1911, Ann. Sci. Éc. Norm. Supér., 28, 33–62.

Tags #

Herglotz theorem, Herglotz–Riesz theorem, Poisson integral, positive harmonic function, positive real part, unit disc

Properties of Herglotz–Riesz functions #

theorem LeanPool.LeanComplexAnalysis.herglotz_integrable (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (w : ℂ) (hw : w ∈ Metric.ball 0 1) :

MeasureTheory.Integrable (fun (x : ↑(Metric.sphere 0 1)) => (↑x + w) / (↑x - w)) ↑μ

The Herglotz-Riesz kernel is integrable on the unit circle.

theorem LeanPool.LeanComplexAnalysis.herglotz_hasDerivAt (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (w₀ : ℂ) (hw₀ : ‖w₀‖ < 1) :

HasDerivAt (fun (w : ℂ) => ∫ (x : ↑(Metric.sphere 0 1)), (↑x + w) / (↑x - w) ∂↑μ) (∫ (x : ↑(Metric.sphere 0 1)), 2 * ↑x / (↑x - w₀) ^ 2 ∂↑μ) w₀

The Herglotz-Riesz representation produces a ℂ differentiable function.

theorem LeanPool.LeanComplexAnalysis.HerglotzRiesz_realPos (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) :

have p := fun (z : ℂ) => ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ; AnalyticOn ℂ p (Metric.ball 0 1) ∧ p 0 = 1 ∧ Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}

Every Herglotz–Riesz representation is analytic, maps 0 to 1 and the unit disc into the right half-plane.

Existence of the Herglotz–Riesz measure #

@[reducible, inline]

abbrev LeanPool.LeanComplexAnalysis.u (p : ℂ → ℂ) (z : ℂ) :

u is the real part of p.

Equations

LeanPool.LeanComplexAnalysis.u p z = (p z).re

Instances For

@[reducible, inline]

abbrev LeanPool.LeanComplexAnalysis.uN (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (z : ℂ) :

uN is u scaled by r n.

Equations

LeanPool.LeanComplexAnalysis.uN p r n z = LeanPool.LeanComplexAnalysis.u p (↑(r n) * z)

Instances For

@[reducible, inline]

abbrev LeanPool.LeanComplexAnalysis.CUnitCircle :

TODO.

Equations

LeanPool.LeanComplexAnalysis.CUnitCircle = C(↑(Metric.sphere 0 1), ℝ )

Instances For

noncomputable def LeanPool.LeanComplexAnalysis.poissonKernelFunc (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

The Poisson kernel function for a fixed z in the unit disc, viewed as a continuous function on the unit circle.

Equations

LeanPool.LeanComplexAnalysis.poissonKernelFunc z hz = { toFun := fun (w : ↑(Metric.sphere 0 1)) => ((↑w + z) / (↑w - z)).re, continuous_toFun := ⋯ }

Instances For

theorem LeanPool.LeanComplexAnalysis.circleMap_mem_unit_circle (t : ℝ) :

circleMap 0 1 t ∈ Metric.sphere 0 1

circleMap takes values on the unit circle.

noncomputable def LeanPool.LeanComplexAnalysis.ΛNVal (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (f : CUnitCircle) :

The value of the functional ΛN on CUnitCircle.

Equations

LeanPool.LeanComplexAnalysis.ΛNVal p r n f = 1 / (2 * Real.pi) * ∫ (t : ℝ) in 0..2 * Real.pi , f ⟨circleMap 0 1 t, ⋯⟩ * LeanPool.LeanComplexAnalysis.uN p r n (circleMap 0 1 t)

Instances For

noncomputable def LeanPool.LeanComplexAnalysis.ΛNLinear (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (h : Continuous (uN p r n ∘ circleMap 0 1)) :

CUnitCircle →ₗ[ℝ ] ℝ

The linear map ΛNLinear.

Equations

LeanPool.LeanComplexAnalysis.ΛNLinear p r n h = { toFun := fun (f : LeanPool.LeanComplexAnalysis.CUnitCircle) => LeanPool.LeanComplexAnalysis.ΛNVal p r n f, map_add' := ⋯, map_smul' := ⋯ }

Instances For

noncomputable def LeanPool.LeanComplexAnalysis.ΛNBound (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) :

The bound ΛNBound for the functional ΛN, defined as 1/2π ∫ t in 0..2*π |uN(e^{it})| dt.

Equations

LeanPool.LeanComplexAnalysis.ΛNBound p r n = 1 / (2 * Real.pi) * ∫ (t : ℝ) in 0..2 * Real.pi , |LeanPool.LeanComplexAnalysis.uN p r n (circleMap 0 1 t)|

Instances For

noncomputable def LeanPool.LeanComplexAnalysis.ΛN (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (h : Continuous (uN p r n ∘ circleMap 0 1)) :

CUnitCircle →L[ℝ ] ℝ

TODO.

Equations

LeanPool.LeanComplexAnalysis.ΛN p r n h = (LeanPool.LeanComplexAnalysis.ΛNLinear p r n h).mkContinuous (LeanPool.LeanComplexAnalysis.ΛNBound p r n) ⋯

Instances For

@[reducible, inline]

abbrev LeanPool.LeanComplexAnalysis.CUnitCircleDual :

TODO.

Equations

LeanPool.LeanComplexAnalysis.CUnitCircleDual = (LeanPool.LeanComplexAnalysis.CUnitCircle →L[ℝ ] ℝ)

Instances For

def LeanPool.LeanComplexAnalysis.K :

Set CUnitCircleDual

TODO.

Equations

LeanPool.LeanComplexAnalysis.K = {Λ : LeanPool.LeanComplexAnalysis.CUnitCircleDual | ∀ (f : LeanPool.LeanComplexAnalysis.CUnitCircle), ‖f‖ < 1 → |Λ f| ≤ 1}

Instances For

def LeanPool.LeanComplexAnalysis.KWeak :

Set (WeakDual ℝ CUnitCircle)

TODO.

Equations

LeanPool.LeanComplexAnalysis.KWeak = LeanPool.LeanComplexAnalysis.K

Instances For

theorem LeanPool.LeanComplexAnalysis.complex_kernel_integrable (μ : MeasureTheory.Measure ↑(Metric.sphere 0 1)) [MeasureTheory.IsFiniteMeasure μ] (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

MeasureTheory.Integrable (fun (w : ↑(Metric.sphere 0 1)) => (↑w + z) / (↑w - z)) μ

The complex Poisson kernel is integrable on the unit circle with respect to any finite measure.

theorem LeanPool.LeanComplexAnalysis.integral_poisson_eq_re_integral (μ : MeasureTheory.Measure ↑(Metric.sphere 0 1)) [MeasureTheory.IsFiniteMeasure μ] (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

∫ (w : ↑(Metric.sphere 0 1)), (poissonKernelFunc z hz) w ∂μ = (∫ (w : ↑(Metric.sphere 0 1)), (↑w + z) / (↑w - z) ∂μ).re

The integral of the Poisson kernel is the real part of the integral of the Herglotz–Riesz kernel.

theorem LeanPool.LeanComplexAnalysis.u_n_pos (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : r n ∈ Set.Ioo 0 1) (z : ℂ) (hz : z ∈ Metric.sphere 0 1) :

0 < uN p r n z

uN p is positive on the unit circle when p takes value in the right half-plane`.

theorem LeanPool.LeanComplexAnalysis.u_n_mean_value (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hr : r n ∈ Set.Ioo 0 1) :

1 / (2 * Real.pi) * ∫ (t : ℝ) in 0..2 * Real.pi , uN p r n (circleMap 0 1 t) = 1

The mean value property for uN p at 0.

theorem LeanPool.LeanComplexAnalysis.u_n_continuous (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hr : r n ∈ Set.Ioo 0 1) :

Continuous (uN p r n ∘ circleMap 0 1)

uN p r n composed with circleMap is continuous.

theorem LeanPool.LeanComplexAnalysis.u_limit_at_z (p : ℂ → ℂ) (r_seq : ℕ → ℝ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hr_lim : Filter.Tendsto r_seq Filter.atTop (nhds 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

Filter.Tendsto (fun (n : ℕ) => u p (↑(r_seq n) * z)) Filter.atTop (nhds (u p z))

The sequence u(p(r_n · z)) converges to u(p(z)) as r_n converges to 1.

theorem LeanPool.LeanComplexAnalysis.harmonic_of_analytic_real (u : ℂ → ℝ) (p : ℂ → ℂ) (hp : AnalyticOn ℂ p (Metric.ball 0 1)) (h_real : ∀ z ∈ Metric.ball 0 1, (p z).re = u z) :

InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)

The real part of an analytic function is harmonic.

theorem LeanPool.LeanComplexAnalysis.poisson_formula_of_harmonicOn_scaled_unitDisc_re_kernel {u : ℂ → ℝ} {z : ℂ} {r : ℝ} (hu : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) (hr : r ∈ Set.Ioo 0 1) (hz : z ∈ Metric.ball 0 1) :

u (↑r * z) = 1 / (2 * Real.pi) * ∫ (t : ℝ) in 0..2 * Real.pi , ((Complex.exp (↑t * Complex.I) + z) / (Complex.exp (↑t * Complex.I) - z)).re * u (↑r * Complex.exp (↑t * Complex.I))

theorem LeanPool.LeanComplexAnalysis.u_approx_eq_Lambda (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hr : r n ∈ Set.Ioo 0 1) (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

u p (↑(r n) * z) = ΛNVal p r n (poissonKernelFunc z hz)

The value of u at r_n * z is equal to the functional ΛN applied to the Poisson kernel at z.

theorem LeanPool.LeanComplexAnalysis.K_eq_polar :

KWeak = WeakDual.polar ℝ (Metric.ball 0 1)

theorem LeanPool.LeanComplexAnalysis.K_weak_compact :

CompactSpace ↑KWeak

We apply the Banach-Alaoglu theorem to show that K is compact in the weak* topology.

noncomputable def LeanPool.LeanComplexAnalysis.denseSeq :

ℕ → CUnitCircle

As a separable space, CUnitCircle contains a dense sequence denseSeq.

Equations

LeanPool.LeanComplexAnalysis.denseSeq = TopologicalSpace.denseSeq LeanPool.LeanComplexAnalysis.CUnitCircle

Instances For

noncomputable def LeanPool.LeanComplexAnalysis.embed (Λ : WeakDual ℝ CUnitCircle) :

TODO.

Equations

LeanPool.LeanComplexAnalysis.embed Λ n = Λ (LeanPool.LeanComplexAnalysis.denseSeq n)

Instances For

theorem LeanPool.LeanComplexAnalysis.embed_continuous :

Continuous embed

theorem LeanPool.LeanComplexAnalysis.embed_injective :

Function.Injective embed

theorem LeanPool.LeanComplexAnalysis.K_weak_metrizable :

TopologicalSpace.MetrizableSpace (Subtype KWeak)

The metrizability of the space KWeak.

theorem LeanPool.LeanComplexAnalysis.norm_lambda_leq_one (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : r n ∈ Set.Ioo 0 1) :

have Λ := ΛN p r n ⋯; ∀ (f : CUnitCircle), ‖f‖ < 1 → |Λ f| ≤ 1

|Λ f| ≤ 1 whenever ‖f‖ < 1.

theorem LeanPool.LeanComplexAnalysis.K_weak_seq_compact :

SeqCompactSpace (Subtype KWeak)

The space KWeak is sequentially compact.

noncomputable def LeanPool.LeanComplexAnalysis.ΛSeq (p : ℂ → ℂ) (r : ℕ → ℝ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hr : ∀ (n : ℕ), r n ∈ Set.Ioo 0 1) (n : ℕ) :

WeakDual ℝ CUnitCircle

The sequence of functionals ΛN.

Equations

LeanPool.LeanComplexAnalysis.ΛSeq p r hp_analytic hr n = LeanPool.LeanComplexAnalysis.ΛN p r n ⋯

Instances For

theorem LeanPool.LeanComplexAnalysis.Λ_seq_mem_K (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : ∀ (k : ℕ), r k ∈ Set.Ioo 0 1) :

ΛSeq p r hp_analytic hr n ∈ KWeak

The sequence ΛSeq is in KWeak.

theorem LeanPool.LeanComplexAnalysis.Λ_seq_converging_subsequence (p : ℂ → ℂ) (r : ℕ → ℝ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : ∀ (n : ℕ), r n ∈ Set.Ioo 0 1) :

∃ (phi : ℕ → ℕ) (Λ : WeakDual ℝ CUnitCircle), StrictMono phi ∧ ∀ (f : CUnitCircle), Filter.Tendsto (fun (k : ℕ) => (ΛSeq p r hp_analytic hr (phi k)) f) Filter.atTop (nhds (Λ f))

There exists a subsequence Λ_{n_k} converging to some Λ in the weak* topology.

theorem LeanPool.LeanComplexAnalysis.Λ_n_nonneg (p : ℂ → ℂ) (r : ℕ → ℝ) (n : ℕ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : r n ∈ Set.Ioo 0 1) :

have Λ := ΛN p r n ⋯; ∀ (f : CUnitCircle), 0 ≤ f → 0 ≤ Λ f

Each ΛN is a positive functional.

theorem LeanPool.LeanComplexAnalysis.riesz_rep (Λ : WeakDual ℝ CUnitCircle) (h_pos : ∀ (f : CUnitCircle), 0 ≤ f → 0 ≤ Λ f) :

∃ (μ : MeasureTheory.Measure ↑(Metric.sphere 0 1)), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (f : CUnitCircle), Λ f = ∫ (z : ↑(Metric.sphere 0 1)), f z ∂μ

We apply the Riesz–Markov–Kakutani representation theorem for Λ to obtain the measure μ.

theorem LeanPool.LeanComplexAnalysis.convergence_sub_seq_functionals (p : ℂ → ℂ) (r : ℕ → ℝ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) (hr : ∀ (n : ℕ), r n ∈ Set.Ioo 0 1) :

∃ (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (phi : ℕ → ℕ), StrictMono phi ∧ ∀ (f : CUnitCircle), 0 ≤ f → Filter.Tendsto (fun (k : ℕ) => (ΛSeq p r hp_analytic hr (phi k)) f) Filter.atTop (nhds (∫ (z : ↑(Metric.sphere 0 1)), f z ∂↑μ))

Convergence of the subsequence of linear functionals.

theorem LeanPool.LeanComplexAnalysis.u_eq_limit_Lambda (p : ℂ → ℂ) (r : ℕ → ℝ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hr : ∀ (n : ℕ), r n ∈ Set.Ioo 0 1) (hr_lim : Filter.Tendsto r Filter.atTop (nhds 1)) (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (phi : ℕ → ℕ) (hphi_strict_mono : StrictMono phi) (hΛ_tendsto : ∀ (f : CUnitCircle), Filter.Tendsto (fun (k : ℕ) => (ΛSeq p r hp_analytic hr (phi k)) f) Filter.atTop (nhds (∫ (z : ↑(Metric.sphere 0 1)), f z ∂↑μ))) (z : ℂ) (hz : z ∈ Metric.ball 0 1) :

u p z = (∫ (w : ↑(Metric.sphere 0 1)), (↑w + z) / (↑w - z) ∂↑μ).re

The value of u at z is equal to the real part of the integral of the Herglotz–Riesz kernel against the measure μ, under hypothesis of weak* convergence of ΛSeq.

theorem LeanPool.LeanComplexAnalysis.analytic_unique_of_real_part (f g : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball 0 1)) (hg : AnalyticOn ℂ g (Metric.ball 0 1)) (h_re : ∀ z ∈ Metric.ball 0 1, (f z).re = (g z).re) (h_zero : f 0 = g 0) :

Set.EqOn f g (Metric.ball 0 1)

If two analytic functions on the unit disc have the same value at 0 and equal real parts, then they are equal on the unit disc.

theorem LeanPool.LeanComplexAnalysis.HerglotzRiesz_representation_existence (p : ℂ → ℂ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (hp_map : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) :

∃ (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)), ∀ z ∈ Metric.ball 0 1, p z = ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ

Every analytic function p on the unit disc with p(0) = 1 and mapping the unit disc to the right half-plane admits a Herglotz–Riesz representation.

Main results #

theorem LeanPool.LeanComplexAnalysis.HerglotzRiesz_representation_analytic (p : ℂ → ℂ) (hp_analytic : AnalyticOn ℂ p (Metric.ball 0 1)) (hp0 : p 0 = 1) (h_real_pos : Set.MapsTo p (Metric.ball 0 1) {w : ℂ | 0 < w.re}) :

∃! μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1), ∀ z ∈ Metric.ball 0 1, p z = ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ

Every analytic function p on the unit disc with p(0) = 1 and mapping the unit disc into the right half-plane admits a unique Herglotz–Riesz representation.

theorem LeanPool.LeanComplexAnalysis.HerglotzRiesz_representation_harmonic (u : ℂ → ℝ) (h_pos : ∀ z ∈ Metric.ball 0 1, 0 < u z) (h_u_zero : u 0 = 1) (h_harmonic : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) :

∃! μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1), ∀ z ∈ Metric.ball 0 1, u z = ∫ (x : ↑(Metric.sphere 0 1)), (1 - ‖z‖ ^ 2) / ‖↑x - z‖ ^ 2 ∂↑μ

Every harmonic function u on the unit disc with u(0) = 1 and u(z) > 0 for all z admits a unique Herglotz–Riesz integral representation.