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 the 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.
• RealRMK.rieszMeasure_integralPositiveLinearMap: the uniqueness of the representing measure in the Riesz–Markov–Kakutani representation theorem.

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] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] : 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 Λ = (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ)).measure

theorem RealRMK.le_rieszMeasure_tsupport_subset {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] {f : CompactlySupportedContinuousMap X ℝ} (hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1) {V : Set X} (hV : tsupport ⇑f ⊆ V) : ENNReal.ofReal (Λ f) ≤ (rieszMeasure Λ) 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] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] {f : CompactlySupportedContinuousMap X ℝ} (hf : ∀ (x : X), 0 ≤ f x) {K : Set X} (hK : IsCompact K) (hfK : ∀ x ∈ K, f x = 1) : (rieszMeasure Λ) 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.

@[simp]

theorem RealRMK.integral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] (f : CompactlySupportedContinuousMap X ℝ) : ∫ (x : X), f x ∂rieszMeasure Λ = Λ 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.

instance RealRMK.regular_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] : (rieszMeasure Λ).Regular

The Riesz measure induced by a positive linear functional on C_c(X, ℝ) is regular.

We show that RealRMK.rieszMeasure is a bijection between positive linear functionals on C_c(X, ℝ) and regular measures with inverse RealRMK.integralPositiveLinearMap.

theorem RealRMK.measure_le_of_isCompact_of_integral {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [ν.OuterRegular] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hμν : ∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν) ⦃K : Set X⦄ (hK : IsCompact K) : μ K ≤ ν K

Note: the assumption IsFiniteMeasureOnCompacts μ cannot be removed. For example, if μ is infinite on any nonempty set and ν = 0, then the hypotheses are satisfied.

theorem MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] {μ ν : Measure X} [LocallyCompactSpace X] [μ.Regular] [ν.Regular] (hμν : ∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) : μ = ν

If two regular measures give the same integral for every function in C_c(X, ℝ), then they are equal.

theorem RealRMK.integralPositiveLinearMap_inj {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [μ.Regular] [ν.Regular] : CompactlySupportedContinuousMap.integralPositiveLinearMap μ = CompactlySupportedContinuousMap.integralPositiveLinearMap ν ↔ μ = ν

Two regular measures are equal iff they induce the same positive linear functional on C_c(X, ℝ).

@[simp]

theorem RealRMK.rieszMeasure_integralPositiveLinearMap {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] {μ : MeasureTheory.Measure X} [LocallyCompactSpace X] [μ.Regular] : rieszMeasure (CompactlySupportedContinuousMap.integralPositiveLinearMap μ) = μ

Every regular measure is induced by a positive linear functional on C_c(X, ℝ). That is, RealRMK.rieszMeasure is a surjective function onto regular measures.

@[simp]

theorem RealRMK.integralPositiveLinearMap_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [LocallyCompactSpace X] : CompactlySupportedContinuousMap.integralPositiveLinearMap (rieszMeasure Λ) = Λ

instance RealRMK.instIsFiniteMeasureRieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) : MeasureTheory.IsFiniteMeasure (rieszMeasure Λ)

theorem MeasureTheory.Measure.exists_regular_eq_of_compactSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (μ : Measure X) [IsFiniteMeasure μ] : ∃ (ν : Measure X), ν.Regular ∧ IsFiniteMeasure ν ∧ ∀ (g : BoundedContinuousFunction X ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν

Given a finite measure on a compact space, there exists another finite measure which integrates in the same way bounded continuous functions, and is regular.

theorem MeasureTheory.Measure.exists_innerRegular_eq_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X) [IsFiniteMeasure μ] {K : Set X} (hK : IsCompact K) (h : μ Kᶜ = 0) : ∃ (ν : Measure X), ν.InnerRegular ∧ IsFiniteMeasure ν ∧ ν Kᶜ = 0 ∧ ∀ (g : BoundedContinuousFunction X ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν

Given a finite measure supported on a compact set, there exists another finite measure which integrates in the same way bounded continuous functions, and is regular.