Commit 2022-04-07 07:05 409f5f28

View on Github →

feat(probability/integration): Bochner integral of the product of independent functions (#13140) This is limited to real-valued functions, which is not very satisfactory but it is not clear (to me) what the most general version of each of those lemmas would be.

Estimated changes

Modified src/probability/integration.lean

added theorem probability_theory.indep_fun.integrable_mul

added theorem probability_theory.indep_fun.integral_mul_of_integrable

added theorem probability_theory.indep_fun.integral_mul_of_nonneg

added theorem probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun'

modified theorem probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun

modified theorem probability_theory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator