Riesz–Markov–Kakutani representation theorem for ℝ≥0

This file proves the Riesz-Markov-Kakutani representation theorem on a locally compact T2 space X for ℝ≥0-linear functionals Λ.

Implementation notes

The proof depends on the version of the theorem for ℝ-linear functional Λ because in a standard proof one has to prove the inequalities by le_antisymm, yet for C_c(X, ℝ≥0) there is no Neg. Here we prove the result by writing ℝ≥0-linear Λ in terms of ℝ-linear toRealLinear Λ and by reducing the statement to the ℝ-version of the theorem.

References

• [Walter Rudin, Real and Complex Analysis.][Rud87]

theorem NNRealRMK.integral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) (f : CompactlySupportedContinuousMap X NNReal) : ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

The Riesz-Markov-Kakutani representation theorem: given a positive linear functional Λ, the (Bochner) integral of f (as a ℝ-valued function) with respect to the rieszMeasure associated to Λ is equal to Λ f.

theorem NNRealRMK.lintegral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) (f : CompactlySupportedContinuousMap X NNReal) : ∫⁻ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

The Riesz-Markov-Kakutani representation theorem: given a positive linear functional Λ, the (lower) Lebesgue integral of f with respect to the rieszMeasure associated to Λ is equal to Λ f.