Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-07 07:54
d6931d91
View on Github →
feat: the covariance of independent random variables is zero (
#27988
)
Estimated changes
Modified
Mathlib/Probability/Independence/Integration.lean
Modified
Mathlib/Probability/Moments/Covariance.lean
added
theorem
ProbabilityTheory.IndepFun.covariance_eq_zero
added
theorem
ProbabilityTheory.covariance_eq_sub