Theorem ProbabilityTheory.measurable_gaussianReal

Modification history

2026-06-03 07:40
Mathlib/Probability/Distributions/Gaussian/Real.lean
feat(gaussianReal): `gaussianReal` is measurable w.r.t. its parameters (#40117) …
Added ProbabilityTheory.measurable_gaussianRealView on Github →