The Riesz–Markov–Kakutani theorem on a compact space

On a compact Hausdorff space X every continuous function is compactly supported, so Mathlib's Riesz–Markov–Kakutani theorem (RealRMK.integral_rieszMeasure), stated for positive linear functionals on C_c(X, ℝ), applies to a linear functional L on C(X, ℝ) that is nonnegative on nonnegative functions: such an L is integration against a regular measure μ. When 0 < L 1, the measure μ is finite and nonzero, with μ X = L 1, so normalizing it gives a regular probability measure ν with ∫ h dν = L h / L 1.

Main results

• LinearMap.exists_regular_integral_eq: a positive linear functional on C(X, ℝ), X compact Hausdorff, is integration against a regular measure.
• LinearMap.exists_isProbabilityMeasure_integral_eq_div: if moreover 0 < L 1, then ∫ h dν = L h / L 1 for a regular probability measure ν.

theorem LinearMap.exists_regular_integral_eq {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (L : C(X, ℝ) →ₗ[ℝ] ℝ) (hL : ∀ (h : C(X, ℝ)), 0 ≤ h → 0 ≤ L h) : ∃ (μ : MeasureTheory.Measure X), μ.Regular ∧ ∀ (h : C(X, ℝ)), ∫ (x : X), h x ∂μ = L h

Riesz–Markov–Kakutani on a compact Hausdorff space: a linear functional on C(X, ℝ) that is nonnegative on nonnegative functions is integration against a regular measure.

theorem LinearMap.exists_isProbabilityMeasure_integral_eq_div {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (L : C(X, ℝ) →ₗ[ℝ] ℝ) (hL1 : 0 < L 1) (hL : ∀ (h : C(X, ℝ)), 0 ≤ h → 0 ≤ L h) : ∃ (ν : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure ν ∧ ν.Regular ∧ ∀ (h : C(X, ℝ)), ∫ (x : X), h x ∂ν = L h / L 1

On a compact Hausdorff space, a linear functional L on C(X, ℝ) that is positive at 1 and nonnegative on nonnegative functions satisfies ∫ h dν = L h / L 1 for a regular probability measure ν.