English
In Real RMK, the integral of f with respect to rieszMeasure equals Λ f, i.e., the real-linear representation agrees with the measure representation.
Русский
В Real RMK интеграл по rieszMeasure равен Λ f, то есть совпадает линейное представление и представление через меру.
LaTeX
$$$\\int f\, d(\\text{rieszMeasure }Λ) = Λ f$.$$
Lean4
/-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,
the integral of `f` with respect to the `rieszMeasure` associated to `Λ` is equal to `Λ f`. -/
theorem integral_rieszMeasure (f : C_c(X, ℝ)) : ∫ x, f x ∂(rieszMeasure Λ) = Λ f := by
-- We apply the result `Λ f ≤ ∫ x, f x ∂(rieszMeasure hΛ)` to `f` and `-f`.
apply le_antisymm
·
calc
_ = -∫ x, (-f) x ∂(rieszMeasure Λ) := by simpa using integral_neg' (-f)
_ ≤ -Λ (-f) := (neg_le_neg (integral_riesz_aux Λ (-f)))
_ = _ := by
simp
-- prove the inequality for `f`
· exact integral_riesz_aux Λ f
