Commit 2024-12-17 01:35 b18fc8a8

feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for NNReal (#18775) Prove additivity of RieszContentAux, completing the proof that it gives a Content. Motivation: this gives the measure related with a positive linear functional Λ on compactly supported continuous functions. The next step is to characterise the constructed measure as the one giving Λ back. In this PR, it is assumed to be NNReal-linear. The main steps to prove additivity have been proposed by @kkytola here. A different approach is taken in #12290 for Real-linear Λ.

• depends on: #12266 for a variation of PartitionOfUnity. The new contents of this PR are contained in MeasureTheory.Integral.linearRieszMarkovKakutani and Topology.ContinuousMap.CompactlySupported.