Commit 2024-02-22 12:56 f2d8a000

View on Github →

feat: Positivity extension for Finset.sum (#10538) Also define a new aesop rule-set and an auxiliary metaprogram proveFinsetNonempty for dealing with Finset.Nonempty conditions. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Order.lean

added def Mathlib.Meta.Positivity.evalFinsetSum

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Created Mathlib/Data/Finset/Attr.lean

Modified Mathlib/Data/Finset/Basic.lean

added def Mathlib.Meta.proveFinsetNonempty

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/LocallyFinite/Basic.lean

modified theorem Finset.nonempty_Ici

modified theorem Finset.nonempty_Ioi

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Finset/Option.lean

Modified Mathlib/Data/Finset/Pi.lean

modified theorem Finset.pi_nonempty

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/Finset/Powerset.lean

modified theorem Finset.powersetCard_nonempty

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Finset/Sigma.lean

Modified Mathlib/Data/Finset/Sups.lean

modified theorem Finset.compls_nonempty

modified theorem Finset.diffs_nonempty

Modified Mathlib/Data/Finset/Sym.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Fintype/Pi.lean

modified theorem Fintype.piFinset_nonempty

Modified scripts/noshake.json

Modified test/positivity.lean