theorem RieszRepresentation.c0_approx_by_cc {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (ε : ℝ) (hε : 0 < ε) : ∃ (g : CompactlySupportedContinuousMap X ℝ), ‖f - { toFun := ⇑g, continuous_toFun := ⋯, zero_at_infty' := ⋯ }‖ ≤ ε

Any continuous function vanishing at infinity can be uniformly approximated to within ε by a continuous function of compact support, via a Urysohn-type cutoff.

theorem riesz_uniqueness {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (μP μN νP νN : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μP] [MeasureTheory.IsFiniteMeasure μN] [MeasureTheory.IsFiniteMeasure νP] [MeasureTheory.IsFiniteMeasure νN] [μP.Regular] [μN.Regular] [νP.Regular] [νN.Regular] (h : ∀ (f : ZeroAtInftyContinuousMap X ℝ), ∫ (x : X), f x ∂μP - ∫ (x : X), f x ∂μN = ∫ (x : X), f x ∂νP - ∫ (x : X), f x ∂νN) (E : Set X) (_hE : MeasurableSet E) : μP.real E - μN.real E = νP.real E - νN.real E

Uniqueness in Riesz representation: two Jordan decompositions of the same continuous linear functional on C₀(X, ℝ) give the same signed measure (on every measurable set).

noncomputable def restrictPositiveCLFToCc {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (hu : ContinuousFunctions.IsPositiveFunctional u) : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

Restrict a positive continuous linear functional on C₀(X, ℝ) to the subspace of compactly supported continuous functions, producing a positive linear functional on C_c(X, ℝ).

theorem rieszMeasure_finite_of_positive_CLF {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (hu : ContinuousFunctions.IsPositiveFunctional u) : MeasureTheory.IsFiniteMeasure (RealRMK.rieszMeasure (restrictPositiveCLFToCc u hu))

The Riesz measure obtained from a positive continuous linear functional on C₀(X, ℝ) is finite, with total mass bounded by ‖u‖.

theorem clf_eq_integral_of_agree_on_cc {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (v : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (hcc : ∀ (g : CompactlySupportedContinuousMap X ℝ), v { toFun := ⇑g, continuous_toFun := ⋯, zero_at_infty' := ⋯ } = ∫ (x : X), g x ∂μ) (f : ZeroAtInftyContinuousMap X ℝ) : v f = ∫ (x : X), f x ∂μ

A continuous linear functional on C₀(X, ℝ) that agrees with integration against a finite measure on every compactly supported continuous function in fact agrees with it on all of C₀(X, ℝ).

theorem riesz_representation {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) : (∃ (μP : MeasureTheory.Measure X) (μN : MeasureTheory.Measure X), MeasureTheory.IsFiniteMeasure μP ∧ MeasureTheory.IsFiniteMeasure μN ∧ μP.Regular ∧ μN.Regular ∧ ∀ (f : ZeroAtInftyContinuousMap X ℝ), u f = ∫ (x : X), f x ∂μP - ∫ (x : X), f x ∂μN) ∧ ∀ (μP μN νP νN : MeasureTheory.Measure X), MeasureTheory.IsFiniteMeasure μP → MeasureTheory.IsFiniteMeasure μN → MeasureTheory.IsFiniteMeasure νP → MeasureTheory.IsFiniteMeasure νN → μP.Regular → μN.Regular → νP.Regular → νN.Regular → (∀ (f : ZeroAtInftyContinuousMap X ℝ), ∫ (x : X), f x ∂μP - ∫ (x : X), f x ∂μN = ∫ (x : X), f x ∂νP - ∫ (x : X), f x ∂νN) → ∀ (E : Set X), MeasurableSet E → μP.real E - μN.real E = νP.real E - νN.real E

Melrose Theorem 4.12 (Riesz representation): every continuous linear functional on C₀(X, ℝ) is uniquely represented as the difference of integrals against two regular finite Borel measures μP - μN on a locally compact metric space.