Uniqueness of the Herglotz–Riesz measure

Main Results

Theorem HerglotzRiesz_representation_uniqueness:

If for two probability measures μ₁ and μ₂ on the unit circle the two functions ∫ x, (x + z) / (x - z) ∂μ₁ and ∫ x, (x + z) / (x - z) ∂μ₂ are identical on the unit disc, then μ₁ = μ₂.

theorem LeanPool.LeanComplexAnalysis.moments_eq_integers (μ₁ μ₂ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (h : ∀ (n : ℕ), ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂↑μ₁ = ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂↑μ₂) (n : ℤ) : ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂↑μ₁ = ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂↑μ₂

Equal moments with natural exponents imply equal moments with integer exponents.

theorem LeanPool.LeanComplexAnalysis.continuous_zpow_on_unit_circle (n : ℤ) : Continuous fun (x : ↑(Metric.sphere 0 1)) => ↑x ^ n

theorem LeanPool.LeanComplexAnalysis.span_moments_dense : (Submodule.span ℂ (Set.range fun (n : ℤ) => { toFun := fun (x : ↑(Metric.sphere 0 1)) => ↑x ^ n, continuous_toFun := ⋯ })).topologicalClosure = ⊤

The span of moments is dense in the space of continuous functions on the unit circle.

theorem LeanPool.LeanComplexAnalysis.integral_eq_on_dense_set {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (S : Submodule ℂ C(X, ℂ)) (hS : S.topologicalClosure = ⊤) (h : ∀ f ∈ S, ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) (f : C(X, ℂ)) : ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν

If two finite measures agree on a dense subspace of continuous functions, then they agree on all continuous functions.

theorem LeanPool.LeanComplexAnalysis.measure_eq_of_moments (μ₁ μ₂ : MeasureTheory.Measure ↑(Metric.sphere 0 1)) [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (h : ∀ (n : ℕ), ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂μ₁ = ∫ (x : ↑(Metric.sphere 0 1)), ↑x ^ n ∂μ₂) : μ₁ = μ₂

If two probability measures on the unit circle have the same moments, then they are equal.

theorem LeanPool.LeanComplexAnalysis.coeffs_eq_of_series_eq (c1 c2 : ℕ → ℂ) (hc1 : ∃ (M : ℝ), ∀ (n : ℕ), ‖c1 n‖ ≤ M) (hc2 : ∃ (M : ℝ), ∀ (n : ℕ), ‖c2 n‖ ≤ M) (h : ∀ (z : ℂ), ‖z‖ < 1 → ∑' (n : ℕ), z ^ (n + 1) * c1 n = ∑' (n : ℕ), z ^ (n + 1) * c2 n) : c1 = c2

If two power series are equal on the unit disc, then their coefficients are equal.

theorem LeanPool.LeanComplexAnalysis.kernel_expansion (z : ℂ) (hz : ‖z‖ < 1) (w : ℂ) (hw : ‖w‖ = 1) : (w + z) / (w - z) = 1 + 2 * ∑' (n : ℕ), z ^ (n + 1) * star (w ^ (n + 1))

We expand the Herglotz–Riesz kernel into a power series at 0 by using that 1/(1 - z/w) = Σ_{n=0}^∞ (z/w)^n.

theorem LeanPool.LeanComplexAnalysis.integral_kernel_expansion (μ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (z : ℂ) (hz : ‖z‖ < 1) : ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ = 1 + 2 * ∑' (n : ℕ), z ^ (n + 1) * ∫ (x : ↑(Metric.sphere 0 1)), star (↑x ^ (n + 1)) ∂↑μ

The kernel_expansion is used to rewrite the integral.

theorem LeanPool.LeanComplexAnalysis.HerglotzRiesz_representation_uniqueness (μ₁ μ₂ : MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)) (h : ∀ z ∈ Metric.ball 0 1, ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ₁ = ∫ (x : ↑(Metric.sphere 0 1)), (↑x + z) / (↑x - z) ∂↑μ₂) : μ₁ = μ₂

If two probability measures on the unit circle yield the same Herglotz–Riesz functions, then they are equal.