Commit 2025-11-24 17:30 e2c1c2db

View on Github →

feat(MeasureTheory): Measure.real of a probability measure (#31942)

Estimated changes

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Fourier/AddCircleMulti.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

Modified Mathlib/MeasureTheory/Measure/Real.lean

deleted theorem MeasureTheory.measureReal_univ_eq_one

added theorem MeasureTheory.probReal_compl_eq_one_sub

added theorem MeasureTheory.probReal_compl_eq_one_sub₀

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

added theorem MeasureTheory.probReal_add_probReal_compl

added theorem MeasureTheory.probReal_univ

Modified Mathlib/Probability/Distributions/Gaussian/Basic.lean

Modified Mathlib/Probability/Moments/Covariance.lean