Theorem MeasureTheory.memLp_id_of_self_sub_integral

Modification history

2025-11-14 10:06
Mathlib/Probability/Moments/CovarianceBilinDual.lean
feat: drop a finiteness assumptions in covariance results (#31569)
Added MeasureTheory.memLp_id_of_self_sub_integralView on Github →