Theorem MeasureTheory.integral_prod_bilin

Modification history

2026-05-23 12:42
Mathlib/MeasureTheory/Integral/Prod.lean
feat: integral of a continuous bilinear map applied to independent random variables (#38754) …
Added MeasureTheory.integral_prod_bilinView on Github →