The Riesz–Markov–Kakutani theorem for order-bounded functionals

Mathlib's Riesz–Markov–Kakutani theorem (RealRMK.integral_rieszMeasure) represents a positive linear functional on C_c(X, ℝ) by a regular measure. A linear functional Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ which is only order bounded, meaning that Λ is bounded above on every order interval [0, f], is represented by the difference of two regular measures, which need not be finite. For instance, a functional bounded in the sup norm on the functions supported in each compact set is order bounded, since 0 ≤ g ≤ f forces tsupport g ⊆ tsupport f and g ≤ f; distributional derivatives of locally finite total variation, tested against continuous functions, are of this kind.

The proof is the Jordan decomposition of Λ. Its positive part Λ⁺ is defined on nonnegative functions by Λ⁺ f = ⨆ { Λ g | 0 ≤ g ≤ f }, which is additive by the Riesz decomposition property of C_c(X, ℝ≥0): a function below f₁ + f₂ is a sum of a function below f₁ and one below f₂. It extends to a positive linear functional on C_c(X, ℝ) (CompactlySupportedContinuousMap.toRealPositiveLinear), and so does the negative part Λ⁻ = Λ⁺ - Λ. The two parts are the least positive functionals dominating Λ and -Λ, and the Riesz measures of Λ⁺ and Λ⁻ represent Λ.

Main declarations

• TauCeti.RealRMK.posPart Λ hΛ, TauCeti.RealRMK.negPart Λ hΛ: the positive and negative parts of an order-bounded linear functional Λ, positive linear functionals with Λ = posPart Λ hΛ - negPart Λ hΛ (TauCeti.RealRMK.posPart_sub_negPart_apply).
• TauCeti.RealRMK.posPart_apply_of_nonneg, TauCeti.RealRMK.negPart_apply_of_nonneg: on a nonnegative f they are the suprema of Λ and of -Λ over [0, f].
• TauCeti.RealRMK.posPart_apply_le_of_le, TauCeti.RealRMK.negPart_apply_le_of_le: minimality among positive functionals dominating Λ and -Λ.
• TauCeti.RealRMK.integral_rieszMeasure_posPart_sub_integral_rieszMeasure_negPart: the Riesz–Markov–Kakutani representation of an order-bounded functional.
• TauCeti.RealRMK.forall_bddAbove_image_Icc_iff_exists_regular: a linear functional on C_c(X, ℝ) is a difference of integrals against two regular measures if and only if it is order bounded.

References

• G. B. Folland, Real Analysis, §7.3: the decomposition of a real functional into positive parts.

noncomputable def TauCeti.RealRMK.posPart {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

The positive part of an order-bounded linear functional Λ on C_c(X, ℝ): the positive linear functional which on a nonnegative f is the supremum of Λ g over 0 ≤ g ≤ f (TauCeti.RealRMK.posPart_apply_of_nonneg). It is the least positive functional dominating Λ on nonnegative functions (TauCeti.RealRMK.posPart_apply_le_of_le).

theorem TauCeti.RealRMK.apply_le_posPart_apply {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f g : CompactlySupportedContinuousMap X ℝ} (hg : 0 ≤ g) (hgf : g ≤ f) : Λ g ≤ (posPart Λ hΛ) f

Every Λ g with 0 ≤ g ≤ f is bounded by the positive part of Λ at f.

theorem TauCeti.RealRMK.posPart_apply_le {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) {c : ℝ} (h : ∀ (g : CompactlySupportedContinuousMap X ℝ), 0 ≤ g → g ≤ f → Λ g ≤ c) : (posPart Λ hΛ) f ≤ c

On a nonnegative f, the positive part of Λ is at most every upper bound of Λ on [0, f].

theorem TauCeti.RealRMK.posPart_apply_of_nonneg {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) : (posPart Λ hΛ) f = ⨆ (g : ↑(Set.Icc 0 f)), Λ ↑g

On a nonnegative f, the positive part of Λ is the supremum of Λ over [0, f].

theorem TauCeti.RealRMK.posPart_apply_le_of_le {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) (P : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) (hP : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → Λ f ≤ P f) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) : (posPart Λ hΛ) f ≤ P f

Minimality of the positive part: a positive functional dominating Λ on nonnegative functions dominates the positive part of Λ there.

noncomputable def TauCeti.RealRMK.negPart {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

The negative part posPart Λ hΛ - Λ of an order-bounded linear functional Λ on C_c(X, ℝ), a positive linear functional. On a nonnegative f it is the supremum of -Λ g over 0 ≤ g ≤ f (TauCeti.RealRMK.negPart_apply_of_nonneg).

@[simp]

theorem TauCeti.RealRMK.negPart_apply {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) (f : CompactlySupportedContinuousMap X ℝ) : (negPart Λ hΛ) f = (posPart Λ hΛ) f - Λ f

The negative part of Λ is its positive part minus Λ.

theorem TauCeti.RealRMK.posPart_sub_negPart_apply {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) (f : CompactlySupportedContinuousMap X ℝ) : (posPart Λ hΛ) f - (negPart Λ hΛ) f = Λ f

The Jordan decomposition Λ = posPart Λ hΛ - negPart Λ hΛ.

theorem TauCeti.RealRMK.neg_apply_le_negPart_apply {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f g : CompactlySupportedContinuousMap X ℝ} (hg : 0 ≤ g) (hgf : g ≤ f) : -Λ g ≤ (negPart Λ hΛ) f

Every -Λ g with 0 ≤ g ≤ f is bounded by the negative part of Λ at f.

theorem TauCeti.RealRMK.negPart_apply_le {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) {c : ℝ} (h : ∀ (g : CompactlySupportedContinuousMap X ℝ), 0 ≤ g → g ≤ f → -Λ g ≤ c) : (negPart Λ hΛ) f ≤ c

On a nonnegative f, the negative part of Λ is at most every upper bound of -Λ on [0, f].

theorem TauCeti.RealRMK.negPart_apply_of_nonneg {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) : (negPart Λ hΛ) f = ⨆ (g : ↑(Set.Icc 0 f)), -Λ ↑g

On a nonnegative f, the negative part of Λ is the supremum of -Λ over [0, f].

theorem TauCeti.RealRMK.negPart_apply_le_of_le {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) (P : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) (hP : ∀ (f : CompactlySupportedContinuousMap X ℝ), 0 ≤ f → -Λ f ≤ P f) {f : CompactlySupportedContinuousMap X ℝ} (hf : 0 ≤ f) : (negPart Λ hΛ) f ≤ P f

Minimality of the negative part: a positive functional dominating -Λ on nonnegative functions dominates the negative part of Λ there.

theorem TauCeti.RealRMK.integral_rieszMeasure_posPart_sub_integral_rieszMeasure_negPart {X : Type u_1} [TopologicalSpace X] {Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ} (hΛ : ∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (f : CompactlySupportedContinuousMap X ℝ) : ∫ (x : X), f x ∂RealRMK.rieszMeasure (posPart Λ hΛ) - ∫ (x : X), f x ∂RealRMK.rieszMeasure (negPart Λ hΛ) = Λ f

The Riesz–Markov–Kakutani representation theorem for an order-bounded linear functional Λ on C_c(X, ℝ): Λ is integration against the Riesz measure of its positive part minus integration against the Riesz measure of its negative part.

theorem TauCeti.RealRMK.forall_bddAbove_image_Icc_iff_exists_regular {X : Type u_1} [TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ) [T2Space X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] : (∀ (f : CompactlySupportedContinuousMap X ℝ), BddAbove (⇑Λ '' Set.Icc 0 f)) ↔ ∃ (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure X), μ.Regular ∧ ν.Regular ∧ ∀ (f : CompactlySupportedContinuousMap X ℝ), Λ f = ∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν

A linear functional on C_c(X, ℝ) is the difference of the integrals against two regular measures if and only if it is order bounded, that is, bounded above on every order interval [0, f]. The two measures need not be finite.