Commit 2023-06-21 03:45 41eb65d5

View on Github →

feat: port Probability.Variance (#5200)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Variance.lean

added theorem MeasureTheory.Memℒp.evariance_lt_top

added theorem MeasureTheory.Memℒp.ofReal_variance_eq

added theorem MeasureTheory.Memℒp.variance_eq

added theorem MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero

added theorem ProbabilityTheory.IndepFun.variance_add

added theorem ProbabilityTheory.IndepFun.variance_sum

added def ProbabilityTheory.evariance

added theorem ProbabilityTheory.evariance_def'

added theorem ProbabilityTheory.evariance_eq_lintegral_ofReal

added theorem ProbabilityTheory.evariance_eq_top

added theorem ProbabilityTheory.evariance_eq_zero_iff

added theorem ProbabilityTheory.evariance_lt_top_iff_memℒp

added theorem ProbabilityTheory.evariance_mul

added theorem ProbabilityTheory.evariance_zero

added theorem ProbabilityTheory.meas_ge_le_evariance_div_sq

added theorem ProbabilityTheory.meas_ge_le_variance_div_sq

added def ProbabilityTheory.variance

added theorem ProbabilityTheory.variance_def'

added theorem ProbabilityTheory.variance_le_expectation_sq

added theorem ProbabilityTheory.variance_mul

added theorem ProbabilityTheory.variance_nonneg

added theorem ProbabilityTheory.variance_smul'

added theorem ProbabilityTheory.variance_smul

added theorem ProbabilityTheory.variance_zero