Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-07 11:59 cf65daf0

View on Github →

feat(probability/variance): define the variance of a random variable, prove its basic properties (#13912)

Estimated changes

Modified docs/undergrad.yaml

Modified src/probability/integration.lean

modified theorem probability_theory.indep_fun.integrable_mul

added theorem probability_theory.indep_fun.integral_mul_of_integrable'

Created src/probability/variance.lean

added theorem probability_theory.indep_fun.variance_add

added theorem probability_theory.indep_fun.variance_sum

added theorem probability_theory.meas_ge_le_variance_div_sq

added def probability_theory.variance

added theorem probability_theory.variance_def'

added theorem probability_theory.variance_le_expectation_sq

added theorem probability_theory.variance_mul

added theorem probability_theory.variance_nonneg

added theorem probability_theory.variance_smul'

added theorem probability_theory.variance_smul

added theorem probability_theory.variance_zero