Commit 2025-07-25 13:19 bf64be8c

View on Github →

feat: covarianceBilin lemmas (#27192) From the Brownian motion project.

Estimated changes

Modified Mathlib/Probability/Moments/CovarianceBilin.lean

added theorem ProbabilityTheory.covarianceBilin_apply'

added theorem ProbabilityTheory.covarianceBilin_comm

added theorem ProbabilityTheory.covarianceBilin_eq_covariance

deleted theorem ProbabilityTheory.covarianceBilin_same_eq_variance

added theorem ProbabilityTheory.covarianceBilin_self_eq_variance

added theorem ProbabilityTheory.covarianceBilin_zero

added theorem ProbabilityTheory.uncenteredCovarianceBilin_zero