Theorem ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp

Modification history

2025-08-06 17:32
Mathlib/Probability/Independence/Integration.lean
feat: integral of product of indepent random variables (#27986) …
Added ProbabilityTheory.IndepFun.integral_fun_comp_mul_compView on Github →