Finite measures are determined by separating test functions

Two finite Borel measures on a Polish space are equal once their integrals agree on a family of real bounded continuous functions that separates points, contains the constant 1 and is closed under multiplication.

This criterion applies when the known integrals are moments of a multiplicative family, such as coordinate monomials or graph homomorphism densities. The constant 1 ensures that the measures have the same total mass.

Without metrizability, a point-separating star subalgebra of bounded continuous functions still determines the integrals of all bounded continuous functions against tight finite measures on a Hausdorff space. On a locally compact Hausdorff space it therefore determines finite inner regular (Radon) measures. Some regularity is needed there: a non-regular Borel measure on a non-metrizable compact space can integrate every continuous function like a point mass. This is the form needed on the Pontryagin dual of a locally compact abelian group that is not second countable.

Main results

• TauCeti.MeasureTheory.ext_of_forall_mem_submonoid_integral_eq_of_polish — two finite Borel measures on a Polish space with the same integrals on a point-separating submonoid of E →ᵇ ℝ are equal.
• TauCeti.MeasureTheory.abs_integral_mulExpNegMulSq_comp_sub_le_of_isTightMeasureSet — the 6 √ε comparison estimate behind the tight case.
• TauCeti.MeasureTheory.integral_eq_of_forall_mem_subalgebra_integral_eq_of_isTightMeasureSet — two tight finite measures on a Hausdorff space with the same integrals on a point-separating star subalgebra of E →ᵇ 𝕜 give the same integral to every real bounded continuous function.
• TauCeti.MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_innerRegular — on a locally compact Hausdorff space, two finite inner regular measures with the same integrals on such a subalgebra are equal.

Implementation notes

The tight case adapts the proofs of Jakob Stiefel's dist_integral_mulExpNegMulSq_comp_le and ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable in Mathlib, which get their compact sets of almost full measure from complete separable metrizability. Here the compact sets come from tightness instead, and Hausdorffness makes them measurable. The passage to measures is Mathlib's uniqueness theorem Measure.ext_of_integral_eq_on_compactlySupported for regular measures.

theorem TauCeti.MeasureTheory.ext_of_forall_mem_submonoid_integral_eq_of_polish {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [PolishSpace E] [BorelSpace E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] {S : Submonoid (BoundedContinuousFunction E ℝ)} (hS : ∀ ⦃x y : E⦄, x ≠ y → ∃ g ∈ S, g x ≠ g y) (heq : ∀ g ∈ S, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') : P = P'

A separating submonoid of test functions determines a finite measure. Two finite Borel measures on a Polish space that give the same integral to every member of a submonoid S of the real bounded continuous functions are equal, provided the members of S separate points.

theorem TauCeti.MeasureTheory.abs_integral_mulExpNegMulSq_comp_sub_le_of_isTightMeasureSet {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [T2Space E] [OpensMeasurableSpace E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] (hP : MeasureTheory.IsTightMeasureSet {P}) (hP' : MeasureTheory.IsTightMeasureSet {P'}) (f : BoundedContinuousFunction E ℝ) {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)} (hA : (Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') {ε : ℝ} (hε : 0 < ε) : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

If two tight finite measures on a Hausdorff space integrate every member of a point-separating real subalgebra A of E →ᵇ ℝ equally, then their integrals of mulExpNegMulSq ε ∘ f differ by at most 6 √ε. This is the tight form of Mathlib's dist_integral_mulExpNegMulSq_comp_le, which assumes a complete second-countable pseudo-metric space instead.

theorem TauCeti.MeasureTheory.integral_eq_of_forall_mem_subalgebra_integral_eq_of_isTightMeasureSet {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [T2Space E] [OpensMeasurableSpace E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] {𝕜 : Type u_2} [RCLike 𝕜] (hP : MeasureTheory.IsTightMeasureSet {P}) (hP' : MeasureTheory.IsTightMeasureSet {P'}) {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') (f : BoundedContinuousFunction E ℝ) : ∫ (x : E), f x ∂P = ∫ (x : E), f x ∂P'

A separating subalgebra determines the integrals of tight measures. Two tight finite measures on a Hausdorff space that integrate every member of a point-separating star subalgebra A of E →ᵇ 𝕜 equally give the same integral to every real bounded continuous function.

theorem TauCeti.MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_innerRegular {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [T2Space E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] {𝕜 : Type u_2} [RCLike 𝕜] [BorelSpace E] [LocallyCompactSpace E] [P.InnerRegular] [P'.InnerRegular] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') : P = P'

A separating subalgebra determines a finite inner regular measure. On a locally compact Hausdorff space, two finite inner regular (equivalently, for finite Borel measures there, regular) measures that integrate every member of a point-separating star subalgebra A of E →ᵇ 𝕜 equally are equal. Unlike MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish, no metrizability or countability is assumed.