positivity core extensions

This file sets up the basic positivity extensions tagged with the @[positivity] attribute.

def Mathlib.Meta.Positivity.evalIte : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form ite p a b, such that positivity successfully recognises both a and b.

Equations

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

def Mathlib.Meta.Positivity.evalMin : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form min a b, such that positivity successfully recognises both a and b.

Equations

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

def Mathlib.Meta.Positivity.evalMax : Mathlib.Meta.Positivity.PositivityExt

Extension for the max operator. The max of two numbers is nonnegative if at least one is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero.

Equations

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

def Mathlib.Meta.Positivity.evalAdd : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form a + b, such that positivity successfully recognises both a and b.

Equations

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

def Mathlib.Meta.Positivity.evalMul : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form a * b, such that positivity successfully recognises both a and b.

Equations

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

def Mathlib.Meta.Positivity.evalIntDiv : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form a / b, where a and b are integers.

Equations

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

def Mathlib.Meta.Positivity.evalPowZeroNat : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form a ^ (0:ℕ). This extension is run in addition to the general a ^ b extension (they are overlapping).

Equations

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

def Mathlib.Meta.Positivity.evalPow : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form a ^ (b : ℕ), such that positivity successfully recognises both a and b.

Equations

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

def Mathlib.Meta.Positivity.evalAbs : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form |a|.

Equations

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

def Mathlib.Meta.Positivity.evalNatAbs : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Int.natAbs is positive when its input is. Since the output type of Int.natAbs is ℕ, the nonnegative case is handled by the default positivity tactic.

def Mathlib.Meta.Positivity.evalNatCast : Mathlib.Meta.Positivity.PositivityExt

def Mathlib.Meta.Positivity.evalIntCast : Mathlib.Meta.Positivity.PositivityExt

def Mathlib.Meta.Positivity.evalNatSucc : Mathlib.Meta.Positivity.PositivityExt

Extension for Nat.succ.

def Mathlib.Meta.Positivity.evalFactorial : Mathlib.Meta.Positivity.PositivityExt

Extension for Nat.factorial.

def Mathlib.Meta.Positivity.evalAscFactorial : Mathlib.Meta.Positivity.PositivityExt

Extension for Nat.ascFactorial.