Hausdorff moment determinacy on a compact interval

Category: 1-Mathlib. No CSD content.

On a compact interval the moment sequence determines the measure. Mathlib provisions both halves — Weierstrass (polynomialFunctions_closure_eq_top) and ext_of_forall_integral_eq_of_IsFiniteMeasure — but does not state the conclusion, so this file assembles it.

The argument is the elementary one: equal moments give equal integrals of polynomials by linearity; polynomials are uniformly dense; and on a finite measure the integral is sup-norm-Lipschitz, so equality passes to every continuous function and then to the measures. No functional-analytic packaging is needed — just a three-term triangle inequality.

Needed by specs/q12c-exponential-characterisation-route.md, where the race property is turned into a moment sequence on [0,1] and determinacy is what converts it back into a distributional identity.

theorem MeasureTheory.integrable_continuousMap {a b : ℝ} (ρ : Measure ↑(Set.Icc a b)) [IsFiniteMeasure ρ] (f : C(↑(Set.Icc a b), ℝ)) : Integrable (fun (x : ↑(Set.Icc a b)) => f x) ρ

A continuous function on a compact space is integrable against a finite measure.

theorem MeasureTheory.abs_integral_le_norm_mul {a b : ℝ} (ρ : Measure ↑(Set.Icc a b)) [IsFiniteMeasure ρ] (f : C(↑(Set.Icc a b), ℝ)) : |∫ (x : ↑(Set.Icc a b)), f x ∂ρ| ≤ ‖f‖ * (ρ Set.univ).toReal

Integrals against a finite measure on a compact space are sup-norm-Lipschitz.

theorem MeasureTheory.integral_polynomial_eq_of_moments {a b : ℝ} {μ ν : Measure ↑(Set.Icc a b)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : ∀ (k : ℕ), ∫ (x : ↑(Set.Icc a b)), ↑x ^ k ∂μ = ∫ (x : ↑(Set.Icc a b)), ↑x ^ k ∂ν) (p : Polynomial ℝ) : ∫ (x : ↑(Set.Icc a b)), Polynomial.eval (↑x) p ∂μ = ∫ (x : ↑(Set.Icc a b)), Polynomial.eval (↑x) p ∂ν

Equal moments give equal integrals of every polynomial.

theorem MeasureTheory.ext_of_forall_integral_pow_eq {a b : ℝ} {μ ν : Measure ↑(Set.Icc a b)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : ∀ (k : ℕ), ∫ (x : ↑(Set.Icc a b)), ↑x ^ k ∂μ = ∫ (x : ↑(Set.Icc a b)), ↑x ^ k ∂ν) : μ = ν

★★ Hausdorff moment determinacy. Two finite Borel measures on a compact interval with the same moment sequence are equal.

The form actually used: measures on ℝ concentrated on the interval

The subtype statement above is the natural one to prove but an awkward one to apply, since the laws one meets in practice are laws of [a,b]-valued random variables and so live on ℝ. This transfers it.

theorem MeasureTheory.ext_of_forall_integral_pow_eq_of_null_compl {a b : ℝ} {μ ν : Measure ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ : μ (Set.Icc a b)ᶜ = 0) (hν : ν (Set.Icc a b)ᶜ = 0) (h : ∀ (k : ℕ), ∫ (x : ℝ), x ^ k ∂μ = ∫ (x : ℝ), x ^ k ∂ν) : μ = ν

★ Continuous functions determined by their moments against powers

The form the Q12-c2 route actually needs, and the one that dissolves its step-3′ fork: no monotone-rearrangement argument and no two-dimensional determinacy, just the same Weierstrass density argument run against a fixed continuous weight.

def MeasureTheory.coordPow {a b : ℝ} (k : ℕ) : C(↑(Set.Icc a b), ℝ)

The k-th coordinate power, bundled.

Equations

• MeasureTheory.coordPow k = { toFun := fun (x : ↑(Set.Icc a b)) => ↑x ^ k, continuous_toFun := ⋯ }

@[simp]

theorem MeasureTheory.coordPow_apply {a b : ℝ} (k : ℕ) (x : ↑(Set.Icc a b)) : (coordPow k) x = ↑x ^ k

theorem MeasureTheory.integrable_mul_continuousMap {a b : ℝ} (ρ : Measure ↑(Set.Icc a b)) [IsFiniteMeasure ρ] (f g : C(↑(Set.Icc a b), ℝ)) : Integrable (fun (x : ↑(Set.Icc a b)) => f x * g x) ρ

theorem MeasureTheory.integrable_mul_pow {a b : ℝ} (ρ : Measure ↑(Set.Icc a b)) [IsFiniteMeasure ρ] (f : C(↑(Set.Icc a b), ℝ)) (k : ℕ) : Integrable (fun (x : ↑(Set.Icc a b)) => f x * ↑x ^ k) ρ

theorem MeasureTheory.integral_mul_polynomial_eq_zero {a b : ℝ} {ρ : Measure ↑(Set.Icc a b)} [IsFiniteMeasure ρ] {d : C(↑(Set.Icc a b), ℝ)} (h : ∀ (k : ℕ), ∫ (x : ↑(Set.Icc a b)), d x * ↑x ^ k ∂ρ = 0) (p : Polynomial ℝ) : ∫ (x : ↑(Set.Icc a b)), d x * Polynomial.eval (↑x) p ∂ρ = 0

A continuous function orthogonal to every power is orthogonal to every polynomial.

theorem MeasureTheory.eq_of_forall_integral_mul_pow_eq {a b : ℝ} {μ : Measure ↑(Set.Icc a b)} [IsFiniteMeasure μ] [μ.IsOpenPosMeasure] {f g : C(↑(Set.Icc a b), ℝ)} (h : ∀ (k : ℕ), ∫ (x : ↑(Set.Icc a b)), f x * ↑x ^ k ∂μ = ∫ (x : ↑(Set.Icc a b)), g x * ↑x ^ k ∂μ) : f = g

★★ Two continuous functions with the same moments against all powers are equal.

IsOpenPosMeasure is what upgrades "equal almost everywhere" to "equal", and it is exactly what a measure with full support on the interval provides.

The carrier: Lebesgue measure on a compact interval

Mathlib has no MeasureSpace instance on the subtype Set.Icc a b, so the measure the results above are stated against has to be built. It is the comap of volume, and it has the two properties they need: finiteness, and full support (which is what turns "equal almost everywhere" into "equal").

noncomputable def MeasureTheory.intervalMeasure (a b : ℝ) : Measure ↑(Set.Icc a b)

Lebesgue measure on a compact interval, as a measure on the subtype.

Equations

• MeasureTheory.intervalMeasure a b = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

instance MeasureTheory.instIsFiniteMeasureIntervalMeasure (a b : ℝ) : IsFiniteMeasure (intervalMeasure a b)

theorem MeasureTheory.isOpenPosMeasure_intervalMeasure {a b : ℝ} (hab : a < b) : (intervalMeasure a b).IsOpenPosMeasure

On a nondegenerate interval the measure has full support, which is what upgrades "equal almost everywhere" to "equal".