Commit 2026-06-03 07:40 6f80c6f7

View on Github →

feat(gaussianReal): gaussianReal is measurable w.r.t. its parameters (#40117) Add measurable_gaussianReal that shows that fun (m, v) => gaussianReal m v is measurable.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.measurable_withDensity

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

modified theorem ProbabilityTheory.measurable_gaussianPDF

modified theorem ProbabilityTheory.measurable_gaussianPDFReal

added theorem ProbabilityTheory.measurable_gaussianReal

added theorem ProbabilityTheory.measurable_uncurry_gaussianPDF

added theorem ProbabilityTheory.measurable_uncurry_gaussianPDFReal

added theorem ProbabilityTheory.stronglyMeasurable_gaussianPDF

added theorem ProbabilityTheory.stronglyMeasurable_uncurry_gaussianPDF

added theorem ProbabilityTheory.stronglyMeasurable_uncurry_gaussianPDFReal