Theorem Integrable.norm_condExp_rpow_le

Modification history

2026-07-02 09:24
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
feat: generalize some lemmas by using conditional Jensen (#36888) …
Added Integrable.norm_condExp_rpow_leView on Github →