Theorem MeasureTheory.measurable_withDensity

Modification history

2026-06-03 07:40
Mathlib/MeasureTheory/Measure/WithDensity.lean
feat(gaussianReal): `gaussianReal` is measurable w.r.t. its parameters (#40117) …
Added MeasureTheory.measurable_withDensityView on Github →