Mathlib v3 is deprecated. Go to Mathlib v4

Theorem probability_theory.indep_fun.integral_mul_of_integrable'

Modification history

2022-08-28 08:57
src/probability/integration.lean
feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167) …
Deleted probability_theory.indep_fun.integral_mul_of_integrable'View on Github →
2022-05-07 11:59
src/probability/integration.lean
feat(probability/variance): define the variance of a random variable, prove its basic properties (#13912)
Added probability_theory.indep_fun.integral_mul_of_integrable'View on Github →