Documentation

Mathlib.Tactic.Positivity.Finset

Positivity extensions for finsets #

This file provides a few positivity extensions that cannot be in either the finset files (because they don't know about ordered fields) or in Tactic.Positivity.Basic (because it doesn't want to know about finiteness).

source
def Mathlib.Meta.Positivity.evalFinsetCard :
Mathlib.Meta.Positivity.PositivityExt

Extension for Finset.card. #s is positive if s is nonempty.

It calls Mathlib.Meta.proveFinsetNonempty to attempt proving that the finset is nonempty.

source
def Mathlib.Meta.Positivity.evalFintypeCard :
Mathlib.Meta.Positivity.PositivityExt

Extension for Fintype.card. Fintype.card α is positive if α is nonempty.

source
def Mathlib.Meta.Positivity.evalFinsetDens :
Mathlib.Meta.Positivity.PositivityExt

Extension for Finset.dens. s.dens is positive if s is nonempty.

It calls Mathlib.Meta.proveFinsetNonempty to attempt proving that the finset is nonempty.

source
def Mathlib.Meta.Positivity.evalFinsetSum :
Mathlib.Meta.Positivity.PositivityExt

The positivity extension which proves that ∑ i ∈ s, f i is nonnegative if f is, and positive if each f i is and s is nonempty.

TODO: The following example does not work

example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum f := by positivity

because compareHyp can't look for assumptions behind binders.