Commit 2024-10-13 20:13 282d392e

View on Github →

chore(Probability/Variance): generalize assumptions from MeasureSpace to MeasurableSpace (#17702) https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60MeasureSpace.60.20vs.20.60Measure.60.20in.20.60ProbabilityTheory.2F.60

Estimated changes

Modified Mathlib/Probability/Variance.lean

modified theorem ProbabilityTheory.IndepFun.variance_add

modified theorem ProbabilityTheory.IndepFun.variance_sum

modified theorem ProbabilityTheory.evariance_def'

modified theorem ProbabilityTheory.meas_ge_le_evariance_div_sq

modified theorem ProbabilityTheory.meas_ge_le_variance_div_sq

modified theorem ProbabilityTheory.variance_def'

modified theorem ProbabilityTheory.variance_le_expectation_sq