Commit 2024-09-28 19:40 4ceb2ea9

View on Github →

feat: order properties of Finset.expect (#16946) Also add a few basic lemmas and fix the delaborator in Algebra.BigOperators.Prereqs. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Expect.lean

added theorem Finset.expect_apply

added theorem Finset.expect_ite_mem

added theorem Fintype.expect_ite_mem

added theorem Fintype.expect_mul_expect

Created Mathlib/Algebra/Order/BigOperators/Expect.lean

added theorem Finset.abs_expect_le_expect_abs

added theorem Finset.exists_lt_of_expect_lt

added theorem Finset.exists_lt_of_lt_expect

added theorem Finset.expect_eq_zero_iff_of_nonneg

added theorem Finset.expect_eq_zero_iff_of_nonpos

added theorem Finset.expect_le

added theorem Finset.expect_le_expect

added theorem Finset.expect_mul_sq_le_sq_mul_sq

added theorem Finset.expect_nonneg

added theorem Finset.expect_pos

added theorem Finset.le_expect

added theorem Finset.le_expect_nonempty_of_subadditive

added theorem Finset.le_expect_nonempty_of_subadditive_on_pred

added theorem Finset.le_expect_of_subadditive

added theorem Finset.le_expect_of_subadditive_on_pred

added theorem Fintype.expect_eq_zero_iff_of_nonneg

added theorem Fintype.expect_eq_zero_iff_of_nonpos

added theorem GCongr.expect_le_expect

added def Mathlib.Meta.Positivity.evalFinsetExpect

Modified Mathlib/Analysis/MeanInequalities.lean

added theorem Real.compact_inner_le_weight_mul_Lp_of_nonneg