feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

[yoh-tanimoto]

define rieszContentAux under Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f) and prove that it is a Content.

Motivation : This will be a basis for example, of the spectral decomposition of self-adjoint operators on Hilbert spaces.

Depends on #12266 for a variation of Urysohn's lemma. Perhaps some refactoring is still needed. More importantly, we should still introduce C_c

Proving (∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), f x ∂(MeasureTheory.Content.measure (rieszContent Λ hΛ)) = Λ f) is available here https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean not yet included in this PR.