Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-07 04:25
09f63ec6
View on Github →
feat: port Probability.Integration (
#4759
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Probability/Integration.lean
added
theorem
ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul
added
theorem
ProbabilityTheory.IndepFun.integrable_mul
added
theorem
ProbabilityTheory.IndepFun.integrable_right_of_integrable_mul
added
theorem
ProbabilityTheory.IndepFun.integral_mul'
added
theorem
ProbabilityTheory.IndepFun.integral_mul
added
theorem
ProbabilityTheory.IndepFun.integral_mul_of_integrable
added
theorem
ProbabilityTheory.IndepFun.integral_mul_of_nonneg
added
theorem
ProbabilityTheory.indepFun_iff_integral_comp_mul
added
theorem
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun''
added
theorem
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
added
theorem
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun
added
theorem
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace
added
theorem
ProbabilityTheory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator