Theorem ProbabilityTheory.IndepFun.covariance_eq_zero

Modification history

2025-10-14 14:50
Mathlib/Probability/Moments/Covariance.lean
chore: notation for (conditional) independence (#30419) …
Modified ProbabilityTheory.IndepFun.covariance_eq_zeroView on Github →
2025-08-07 07:54
Mathlib/Probability/Moments/Covariance.lean
feat: the covariance of independent random variables is zero (#27988)
Added ProbabilityTheory.IndepFun.covariance_eq_zeroView on Github →