Commit 2025-02-05 09:36 6449d921

feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure (#20040) Prove regularity of RieszContent, define the Riesz measure μ Λ and prove basic properties. Motivation: these definitions and lemmas will be used to prove the Riesz-Markov-Kakutani theorem, characterizing μ Λ. In this PR, it is assumed to be NNReal-linear. In this way, the proof of the RMK theorem will be twice as long as a proof for Real-linear Λ because one cannot define -f. #12290 proves the RMK theorem for real linear Λ, using the Riesz measure defined in this PR through toNNRealLinear.