Commit 2025-06-09 12:09 c9a191be
View on Github →feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for NNReal-linear functionals (#24265)
prove the Riesz-Markov-Kakutani theorem for NNReal-linear functional, by reducing the statement to the Real-version, but for lintegral instead of integral.
The bulk of the PR is the definitions and lemmas to go back and forth between Real and NNReal linear functionals.
Motivation: this is the version first aimed at, perhaps for applications in probability.