Documentation

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Riesz–Markov–Kakutani representation theorem for ℝ≥0 #

This file proves the Riesz-Markov-Kakutani representation theorem on a locally compact T2 space X for ℝ≥0-linear functionals Λ.

Implementation notes #

The proof depends on the version of the theorem for ℝ-linear functional Λ because in a standard proof one has to prove the inequalities by le_antisymm, yet for C_c(X, ℝ≥0) there is no Neg. Here we prove the result by writing ℝ≥0-linear Λ in terms of ℝ-linear toRealLinear Λ and by reducing the statement to the ℝ-version of the theorem.

References #

source
@[simp]
theorem NNRealRMK.integral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) (f : CompactlySupportedContinuousMap X NNReal) :
∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

The Riesz-Markov-Kakutani representation theorem: given a positive linear functional Λ, the (Bochner) integral of f (as a ℝ-valued function) with respect to the rieszMeasure associated to Λ is equal to Λ f.

source
@[simp]
theorem NNRealRMK.lintegral_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) (f : CompactlySupportedContinuousMap X NNReal) :
∫⁻ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

The Riesz-Markov-Kakutani representation theorem: given a positive linear functional Λ, the (lower) Lebesgue integral of f with respect to the rieszMeasure associated to Λ is equal to Λ f.

source
instance NNRealRMK.rieszMeasure_regular {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) :
(rieszMeasure Λ).Regular

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

We show that NNRealRMK.rieszMeasure is a bijection between linear functionals on C_c(X, ℝ≥0) and regular measures with inverse NNRealRMK.integralLinearMap.

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

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

source
@[simp]
theorem NNRealRMK.integralLinearMap_inj {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {μ ν : MeasureTheory.Measure X} [μ.Regular] [ν.Regular] :
CompactlySupportedContinuousMap.integralLinearMap μ = CompactlySupportedContinuousMap.integralLinearMap ν ↔ μ = ν

If two regular measures induce the same linear functional on C_c(X, ℝ≥0), then they are equal.

source
@[simp]
theorem NNRealRMK.rieszMeasure_integralLinearMap {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] {μ : MeasureTheory.Measure X} [μ.Regular] :
rieszMeasure (CompactlySupportedContinuousMap.integralLinearMap μ) = μ

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

source
@[simp]
theorem NNRealRMK.integralLinearMap_rieszMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) :
CompactlySupportedContinuousMap.integralLinearMap (rieszMeasure Λ) = Λ