Theorem ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul
Modification history
2025-08-06 17:32
Mathlib/Probability/Independence/Integration.lean
feat: integral of product of indepent random variables (#27986) …
Modified ProbabilityTheory.IndepFun.integrable_left_of_integrable_mulView on Github →