Riesz–Markov–Kakutani representation theorem for real-linear functionals

The Riesz–Markov–Kakutani representation theorem relates linear functionals on spaces of continuous functions on a locally compact space to measures.

There are many closely related variations of the theorem. This file contains that proof of the version where the space is a locally compact T2 space, the linear functionals are real and the continuous functions have compact support.

Main definitions & statements

• RealRMK.rieszMeasure: the measure induced by a real linear positive functional.
• RealRMK.integral_rieszMeasure: the Riesz–Markov–Kakutani representation theorem for a real linear positive functional.

Implementation notes

The measure is defined through rieszContent which is for NNReal using the toNNRealLinear version of Λ.

The Riesz–Markov–Kakutani representation theorem is first proved for Real-linear Λ because equality is proven using two inequalities by considering Λ f and Λ (-f) for all functions f, yet on C_c(X, ℝ≥0) there is no negation.

References

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

noncomputable def RealRMK.rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → 0 ≤ Λ f) : MeasureTheory.Measure X

The measure induced for Real-linear positive functional Λ, defined through toNNRealLinear and the NNReal-version of rieszContent. This is under the namespace RealRMK, while rieszMeasure without namespace is for NNReal-linear Λ.

Equations

• RealRMK.rieszMeasure hΛ = (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ hΛ)).measure

theorem RealRMK.le_rieszMeasure_tsupport_subset {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → 0 ≤ Λ f) {f : CompactlySupportedContinuousMap X ℝ} (hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1) {V : Set X} (hV : tsupport ⇑f ⊆ V) : ENNReal.ofReal (Λ f) ≤ (rieszMeasure hΛ) V

If f assumes values between 0 and 1 and the support is contained in V, then Λ f ≤ rieszMeasure V.

theorem RealRMK.rieszMeasure_le_of_eq_one {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → 0 ≤ Λ f) {f : CompactlySupportedContinuousMap X ℝ} (hf : ∀ (x : X), 0 ≤ f x) {K : Set X} (hK : IsCompact K) (hfK : ∀ x ∈ K, f x = 1) : (rieszMeasure hΛ) K ≤ ENNReal.ofReal (Λ f)

If f assumes the value 1 on a compact set K then rieszMeasure K ≤ Λ f.

theorem RealRMK.range_cut_partition {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (f : CompactlySupportedContinuousMap X ℝ) (a : ℝ) {ε : ℝ} (hε : 0 < ε) (N : ℕ) (hf : Set.range ⇑f ⊆ Set.Ioo a (a + ↑N * ε)) : ∃ (E : Fin N → Set X), tsupport ⇑f = ⋃ (j : Fin N), E j ∧ Set.univ.PairwiseDisjoint E ∧ (∀ (n : Fin N), ∀ x ∈ E n, a + ε * ↑↑n < f x ∧ f x ≤ a + ε * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)

Given f : C_c(X, ℝ) such that range f ⊆ [a, b] we obtain a partition of the support of f determined by partitioning [a, b] into N pieces.

theorem RealRMK.exists_open_approx {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (f : CompactlySupportedContinuousMap X ℝ) {ε : ℝ} (hε : 0 < ε) (E : Set X) {μ : MeasureTheory.Content X} (hμ : μ.outerMeasure E ≠ ⊤) (hμ' : MeasurableSet E) {c : ℝ} (hfE : ∀ x ∈ E, f x < c) : ∃ (V : TopologicalSpace.Opens X), E ⊆ ↑V ∧ (∀ x ∈ V, f x < c) ∧ μ.measure ↑V ≤ μ.measure E + ENNReal.ofReal ε

Given a set E, a function f : C_c(X, ℝ), 0 < ε and ∀ x ∈ E, f x < c, there exists an open set V such that E ⊆ V and the sets are similar in measure and ∀ x ∈ V, f x < c.

theorem RealRMK.integral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → 0 ≤ Λ f) (f : CompactlySupportedContinuousMap X ℝ) : ∫ (x : X), f x ∂rieszMeasure hΛ = Λ f

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