English
The Riesz-Markov-Kakutani theorem yields that the integral of f with respect to rieszMeasure Λ equals Λ f for f ∈ C_c(X,ℝ≥0).
Русский
Теорема Рiesz-Маркoв-Какутани даёт, что интеграл по rieszMeasure Λ равен Λ f для f ∈ C_c(X,ℝ≥0).
LaTeX
$$$\\int_X f \\; d(\\text{rieszMeasure }Λ) = Λ f$ for f ∈ C_c(X,ℝ≥0).$$
Lean4
/-- 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`. -/
theorem lintegral_rieszMeasure (f : C_c(X, ℝ≥0)) : ∫⁻ (x : X), f x ∂(rieszMeasure Λ) = Λ f :=
by
rw [lintegral_coe_eq_integral, ← ENNReal.ofNNReal_toNNReal]
· rw [ENNReal.coe_inj, Real.toNNReal_of_nonneg (MeasureTheory.integral_nonneg (by intro a; simp)), NNReal.eq_iff,
NNReal.coe_mk]
exact integral_rieszMeasure Λ f
rw [rieszMeasure]
exact Continuous.integrable_of_hasCompactSupport (by fun_prop) (HasCompactSupport.comp_left f.hasCompactSupport rfl)
