Riesz–Markov–Kakutani representation theorem

This file will prove different versions of the Riesz-Markov-Kakutani representation theorem. The theorem is first proven for compact spaces, from which the statements about linear functionals on bounded continuous functions or compactly supported functions on locally compact spaces follow.

To make use of the existing API, the measure is constructed from a content λ on the compact subsets of the 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] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal) : TopologicalSpace.Compacts X → NNReal

Given a positive linear functional Λ on X, for K ⊆ X compact define λ(K) = inf {Λf | 1≤f on K}. When X is a compact Hausdorff 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 : BoundedContinuousFunction X NNReal | ∀ x ∈ K, 1 ≤ f x})

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

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

theorem rieszContentAux_mono {X : Type u_1} [TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal) {K₁ : TopologicalSpace.Compacts X} {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] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal) {K : TopologicalSpace.Compacts X} {f : BoundedContinuousFunction X NNReal} (h : ∀ x ∈ K, 1 ≤ f x) : rieszContentAux Λ K ≤ Λ f

Any bounded 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] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal) (K : TopologicalSpace.Compacts X) {ε : NNReal} (εpos : 0 < ε) : ∃ (f : BoundedContinuousFunction 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 bounded 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] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal) (K1 : TopologicalSpace.Compacts X) (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.