Theorem ProbabilityTheory.aemeasurable_exp_mul

Modification history

2025-01-03 11:53
Mathlib/Probability/Moments.lean
feat: `fun ω ↦ exp (t * X ω)` is integrable if `X` is bounded above (#20017) …
Added ProbabilityTheory.aemeasurable_exp_mulView on Github →