Commit 2022-08-28 08:57 de62604b

feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167) The integral of a product of independent random variables is the product of the integrals. This is already in mathlib when the random variables are integrable, but it also holds when they are not integrable (as both sides are then zero). In this PR, we remove the integrability assumption from this statement (and weaken accordingly further results that depended on this one).