Commit 2025-04-12 08:23 0c2287c9

feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for Real-linear functionals (#12290) Prove that rieszContent gives a measure rieszMeasure such that, under Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f), it holds that ∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), f x ∂ (rieszMeasure Λ hΛ) = Λ f. The measure is defined through rieszContent for toNNRealLinear-version of Λ. The result is first proved for Real-linear Λ because in a standard proof one has to prove the inequalities by considering Λ f and Λ (-f) for all functions f, yet on C_c(X, ℝ≥0) there is no negation.