English
The Riesz content λ is the content on X defined by λ(K) = rieszContentAux Λ K with regularity and subadditivity properties.
Русский
Контент Рiesz λ определяется как λ(K) = rieszContentAux Λ K и обладает регулярностью и субаддитивностью.
LaTeX
$$$\\lambda = \\lambda_{Λ} : \\mathcal{C}(X) \\to \\mathbb{R}_{+}$, with λ(K) = rieszContentAux Λ K and properties listed.$$
Lean4
/-- 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`. -/
theorem integral_rieszMeasure (f : C_c(X, ℝ≥0)) : ∫ (x : X), (f x : ℝ) ∂(rieszMeasure Λ) = Λ f :=
by
rw [← eq_toRealPositiveLinear_toReal Λ f, ← RealRMK.integral_rieszMeasure (toRealPositiveLinear Λ) f.toReal]
simp [RealRMK.rieszMeasure, NNRealRMK.rieszMeasure]
