Theorem ProbabilityTheory.IndepFun.integral_smul_eq_smul_integral

Modification history

2026-05-23 12:42
Mathlib/Probability/Independence/Integration.lean
feat: integral of a continuous bilinear map applied to independent random variables (#38754) …
Added ProbabilityTheory.IndepFun.integral_smul_eq_smul_integralView on Github →