Documentation

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani

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 #

Construction of the content: #

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
Instances For

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

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

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

    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) + ε.

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