Scalar measures are determined by their integrals of continuous functions

Let X be a locally compact Hausdorff space with its Borel σ-algebra and let 𝕜 be ℝ or ℂ (any RCLike field). A 𝕜-valued measure μ on X whose variation |μ| is regular is determined by the integrals ∫ f dμ of the compactly supported continuous real functions f. This is the uniqueness half of the Riesz representation theorem for the dual of C₀(X, 𝕜); for positive measures it is Mathlib's MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported.

On a compact space every continuous function is compactly supported, so a scalar measure of regular variation on a compact Hausdorff space is determined by its integrals of the functions in C(X, 𝕜). This is how a measure is identified when only its action on continuous functions is known, as for the polarized measures B ↦ ⟪ξ, P(B) ψ⟫ attached to a representation of C(X, ℂ) on a Hilbert space.

Regularity cannot be dropped: on a non-metrizable compact space there are distinct Borel probability measures with the same integral for every continuous function. The variation of a scalar measure is always finite (MeasureTheory.VectorMeasure.isFiniteMeasure_variation), so regularity of |μ| is the only hypothesis.

Main results

• MeasureTheory.VectorMeasure.eq_zero_of_integral_eq_zero_on_compactlySupported: a scalar measure of regular variation whose integral vanishes on C_c(X, ℝ) is zero.
• MeasureTheory.VectorMeasure.ext_of_integral_eq_on_compactlySupported: two scalar measures of regular variation with the same integrals on C_c(X, ℝ) are equal.
• MeasureTheory.VectorMeasure.eq_zero_of_integral_eq_zero_on_continuousMap, MeasureTheory.VectorMeasure.ext_of_integral_eq_on_continuousMap: the same on a compact space, tested against C(X, 𝕜).

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw–Hill (1987), Theorem 6.19.

theorem MeasureTheory.VectorMeasure.eq_zero_of_integral_eq_zero_on_compactlySupported {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [RCLike 𝕜] [LocallyCompactSpace X] (μ : VectorMeasure X 𝕜) [μ.variation.Regular] (h : ∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = 0) : μ = 0

Uniqueness of scalar measures. On a locally compact Hausdorff space, a scalar measure of regular variation whose integral vanishes on every compactly supported continuous real function is zero.

theorem MeasureTheory.VectorMeasure.ext_of_integral_eq_on_compactlySupported {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [RCLike 𝕜] [LocallyCompactSpace X] {μ ν : VectorMeasure X 𝕜} [μ.variation.Regular] [ν.variation.Regular] (h : ∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = ∫ᵛ (x : X), ↑(f x) ∂[ContinuousLinearMap.mul ℝ 𝕜; ν]) : μ = ν

Uniqueness of scalar measures. On a locally compact Hausdorff space, two scalar measures of regular variation with the same integral of every compactly supported continuous real function are equal.

theorem MeasureTheory.VectorMeasure.eq_zero_of_integral_eq_zero_on_continuousMap {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [RCLike 𝕜] [CompactSpace X] (μ : VectorMeasure X 𝕜) [μ.variation.Regular] (h : ∀ (f : C(X, 𝕜)), ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = 0) : μ = 0

Uniqueness of scalar measures. On a compact Hausdorff space, a scalar measure of regular variation whose integral vanishes on C(X, 𝕜) is zero.

theorem MeasureTheory.VectorMeasure.ext_of_integral_eq_on_continuousMap {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [RCLike 𝕜] [CompactSpace X] {μ ν : VectorMeasure X 𝕜} [μ.variation.Regular] [ν.variation.Regular] (h : ∀ (f : C(X, 𝕜)), ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; μ] = ∫ᵛ (x : X), f x ∂[ContinuousLinearMap.mul ℝ 𝕜; ν]) : μ = ν

Uniqueness of scalar measures. On a compact Hausdorff space, two scalar measures of regular variation with the same integral of every function in C(X, 𝕜) are equal.