Commit 2024-10-21 10:47 d43bc00b

View on Github →

feat: Popoviciu's inequality (#17868) Formalize Popoviciu's inequality on variances through the Bhatia-Davis inequality.

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.memℒp_of_bounded

Modified Mathlib/Probability/Variance.lean

added theorem ProbabilityTheory.variance_le_sq_of_bounded

added theorem ProbabilityTheory.variance_le_sub_mul_sub