Riesz–Markov–Kakutani representation theorem

This file will prove the Riesz-Markov-Kakutani representation theorem on a locally compact T2 space X. As a special case, the statements about linear functionals on bounded continuous functions follows.

To make use of the existing API, the measure is constructed from a content λ on the compact subsets of a locally compact space X, rather than the usual construction of open sets in the literature.

References

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

Construction of the content:

def rieszContentAux {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) : TopologicalSpace.Compacts X → NNReal

Given a positive linear functional Λ on continuous compactly supported functions on X with values in ℝ≥0, for K ⊆ X compact define λ(K) = inf {Λf | 1≤f on K}. When X is a locally compact T2 space, this will be shown to be a content, and will be shown to agree with the Riesz measure on the compact subsets K ⊆ X.

Equations

• rieszContentAux Λ K = sInf (⇑Λ '' {f : CompactlySupportedContinuousMap X NNReal | ∀ x ∈ K, 1 ≤ f x})

theorem rieszContentAux_image_nonempty {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) [T2Space X] [LocallyCompactSpace X] (K : TopologicalSpace.Compacts X) : (⇑Λ '' {f : CompactlySupportedContinuousMap X NNReal | ∀ x ∈ K, 1 ≤ f x}).Nonempty

For any compact subset K ⊆ X, there exist some compactly supported continuous nonnegative functions f on X such that f ≥ 1 on K.

theorem rieszContentAux_mono {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) [T2Space X] [LocallyCompactSpace X] {K₁ K₂ : TopologicalSpace.Compacts X} (h : K₁ ≤ K₂) : rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂

Riesz content λ (associated with a positive linear functional Λ) is monotone: if K₁ ⊆ K₂ are compact subsets in X, then λ(K₁) ≤ λ(K₂).

theorem rieszContentAux_le {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) {K : TopologicalSpace.Compacts X} {f : CompactlySupportedContinuousMap X NNReal} (h : ∀ x ∈ K, 1 ≤ f x) : rieszContentAux Λ K ≤ Λ f

Any compactly supported continuous nonnegative f such that f ≥ 1 on K gives an upper bound on the content of K; namely λ(K) ≤ Λ f.

theorem exists_lt_rieszContentAux_add_pos {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) [T2Space X] [LocallyCompactSpace X] (K : TopologicalSpace.Compacts X) {ε : NNReal} (εpos : 0 < ε) : ∃ (f : CompactlySupportedContinuousMap X NNReal), (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

The Riesz content can be approximated arbitrarily well by evaluating the positive linear functional on test functions: for any ε > 0, there exists a compactly supported continuous nonnegative function f on X such that f ≥ 1 on K and such that λ(K) ≤ Λ f < λ(K) + ε.

theorem rieszContentAux_sup_le {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) [T2Space X] [LocallyCompactSpace X] (K1 K2 : TopologicalSpace.Compacts X) : rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2

The Riesz content λ associated to a given positive linear functional Λ is finitely subadditive: λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂) for any compact subsets K₁, K₂ ⊆ X.

theorem exists_continuous_add_one_of_isCompact_nnreal {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] {s₀ s₁ t : Set X} (s₀_compact : IsCompact s₀) (s₁_compact : IsCompact s₁) (t_compact : IsCompact t) (disj : Disjoint s₀ s₁) (hst : s₀ ∪ s₁ ⊆ t) : ∃ (f₀ : CompactlySupportedContinuousMap X NNReal) (f₁ : CompactlySupportedContinuousMap X NNReal), Set.EqOn (⇑f₀) 1 s₀ ∧ Set.EqOn (⇑f₁) 1 s₁ ∧ Set.EqOn (⇑(f₀ + f₁)) 1 t

theorem rieszContentAux_union {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) [T2Space X] [LocallyCompactSpace X] {K₁ K₂ : TopologicalSpace.Compacts X} (disj : Disjoint ↑K₁ ↑K₂) : rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂

noncomputable def rieszContent {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) : MeasureTheory.Content X

The content induced by the linear functional Λ.

Equations

• rieszContent Λ = { toFun := rieszContentAux Λ, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }