Theorem Real.aemeasurable_of_aemeasurable_exp_mul

Modification history

2025-01-08 08:24
Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
feat: misc. lemmas about moments, tilted measures (#20150)
Added Real.aemeasurable_of_aemeasurable_exp_mulView on Github →