Riesz–Markov–Kakutani representation theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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: #

source

noncomputable def riesz_content_aux {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) :

topological_space.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

riesz_content_aux Λ = λ (K : topological_space.compacts X), has_Inf.Inf (⇑Λ '' {f : bounded_continuous_function X nnreal | ∀ (x : X), x ∈ K → 1 ≤ ⇑f x})

source

theorem riesz_content_aux_image_nonempty {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) (K : topological_space.compacts X) :

(⇑Λ '' {f : bounded_continuous_function X nnreal | ∀ (x : X), 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.

source

theorem riesz_content_aux_mono {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) {K₁ K₂ : topological_space.compacts X} (h : K₁ ≤ K₂) :

riesz_content_aux Λ K₁ ≤ riesz_content_aux Λ K₂

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

source

theorem riesz_content_aux_le {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) {K : topological_space.compacts X} {f : bounded_continuous_function X nnreal} (h : ∀ (x : X), x ∈ K → 1 ≤ ⇑f x) :

riesz_content_aux Λ 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.

source

theorem exists_lt_riesz_content_aux_add_pos {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) (K : topological_space.compacts X) {ε : nnreal} (εpos : 0 < ε) :

∃ (f : bounded_continuous_function X nnreal), (∀ (x : X), x ∈ K → 1 ≤ ⇑f x) ∧ ⇑Λ f < riesz_content_aux Λ 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) + ε.

source

theorem riesz_content_aux_sup_le {X : Type u_1} [topological_space X] (Λ : bounded_continuous_function X nnreal →ₗ[nnreal ] nnreal) (K1 K2 : topological_space.compacts X) :

riesz_content_aux Λ (K1 ⊔ K2) ≤ riesz_content_aux Λ K1 + riesz_content_aux Λ 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.