Commit 2024-12-17 01:35 b18fc8a8
View on Github →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 inMeasureTheory.Integral.linearRieszMarkovKakutani
andTopology.ContinuousMap.CompactlySupported
.