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).

def Mathlib.Meta.Positivity.evalFinsetCard : 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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalFintypeCard : PositivityExt

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalFinsetDens : 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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalFinsetSum : 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.