positivity core extensions

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

theorem Mathlib.Meta.Positivity.ite_pos {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [LT α] (ha : 0 < a) (hb : 0 < b) : 0 < if p then a else b

theorem Mathlib.Meta.Positivity.ite_nonneg {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [LE α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ if p then a else b

theorem Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [Preorder α] (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ if p then a else b

theorem Mathlib.Meta.Positivity.ite_nonneg_of_nonneg_of_pos {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [Preorder α] (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ if p then a else b

theorem Mathlib.Meta.Positivity.ite_ne_zero {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (if p then a else b) ≠ 0

theorem Mathlib.Meta.Positivity.ite_ne_zero_of_pos_of_ne_zero {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [Preorder α] (ha : 0 < a) (hb : b ≠ 0) : (if p then a else b) ≠ 0

theorem Mathlib.Meta.Positivity.ite_ne_zero_of_ne_zero_of_pos {α : Type u_1} [Zero α] (p : Prop) [Decidable p] {a b : α} [Preorder α] (ha : a ≠ 0) (hb : 0 < b) : (if p then a else b) ≠ 0

def Mathlib.Meta.Positivity.evalIte : PositivityExt

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

theorem Mathlib.Meta.Positivity.le_min_of_lt_of_le {R : Type u_2} [LinearOrder R] {a b c : R} (ha : a < b) (hb : a ≤ c) : a ≤ min b c

theorem Mathlib.Meta.Positivity.le_min_of_le_of_lt {R : Type u_2} [LinearOrder R] {a b c : R} (ha : a ≤ b) (hb : a < c) : a ≤ min b c

theorem Mathlib.Meta.Positivity.min_ne {R : Type u_2} [LinearOrder R] {a b c : R} (ha : a ≠ c) (hb : b ≠ c) : min a b ≠ c

theorem Mathlib.Meta.Positivity.min_ne_of_ne_of_lt {R : Type u_2} [LinearOrder R] {a b c : R} (ha : a ≠ c) (hb : c < b) : min a b ≠ c

theorem Mathlib.Meta.Positivity.min_ne_of_lt_of_ne {R : Type u_2} [LinearOrder R] {a b c : R} (ha : c < a) (hb : b ≠ c) : min a b ≠ c

theorem Mathlib.Meta.Positivity.max_ne {R : Type u_2} [LinearOrder R] {a b c : R} (ha : a ≠ c) (hb : b ≠ c) : max a b ≠ c

def Mathlib.Meta.Positivity.evalMin : PositivityExt

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

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

def Mathlib.Meta.Positivity.evalAdd : PositivityExt

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

def Mathlib.Meta.Positivity.evalMul : PositivityExt

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

theorem Mathlib.Meta.Positivity.int_div_self_pos {a : ℤ} (ha : 0 < a) : 0 < a / a

theorem Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_nonneg {a b : ℤ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b

theorem Mathlib.Meta.Positivity.int_div_nonneg_of_nonneg_of_pos {a b : ℤ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b

theorem Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 ≤ a / b

def Mathlib.Meta.Positivity.evalIntDiv : PositivityExt

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

theorem Mathlib.Meta.Positivity.pow_zero_pos {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] (a : α) : 0 < a ^ 0

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

def Mathlib.Meta.Positivity.evalPow : PositivityExt

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

theorem Mathlib.Meta.Positivity.abs_pos_of_ne_zero {α : Type u_2} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} : a ≠ 0 → 0 < |a|

def Mathlib.Meta.Positivity.evalAbs : PositivityExt

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

theorem Mathlib.Meta.Positivity.int_natAbs_pos {n : ℤ} (hn : 0 < n) : 0 < n.natAbs

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

Extension for the positivity tactic: Nat.cast is always non-negative, and positive when its input is.

def Mathlib.Meta.Positivity.evalIntCast : PositivityExt

Extension for the positivity tactic: Int.cast is positive (resp. non-negative) if its input is.

def Mathlib.Meta.Positivity.evalNatSucc : PositivityExt

Extension for Nat.succ.

def Mathlib.Meta.Positivity.evalPNatVal : PositivityExt

Extension for PNat.val.

def Mathlib.Meta.Positivity.evalFactorial : PositivityExt

Extension for Nat.factorial.

def Mathlib.Meta.Positivity.evalAscFactorial : PositivityExt

Extension for Nat.ascFactorial.

def Mathlib.Meta.Positivity.evalNatGCD : PositivityExt

Extension for Nat.gcd. Uses positivity of the left term, if available, then tries the right term.

The implementation relies on the fact that Positivity.core on ℕ never returns nonzero.

def Mathlib.Meta.Positivity.evalNatLCM : PositivityExt

Extension for Nat.lcm.

def Mathlib.Meta.Positivity.evalNatSqrt : PositivityExt

Extension for Nat.sqrt.

def Mathlib.Meta.Positivity.evalIntGCD : PositivityExt

Extension for Int.gcd. Uses positivity of the left term, if available, then tries the right term.

def Mathlib.Meta.Positivity.evalIntLCM : PositivityExt

Extension for Int.lcm.

theorem Mathlib.Meta.Positivity.NNRat.num_pos_of_pos {q : ℚ≥0} : 0 < q → 0 < q.num

Alias of the reverse direction of NNRat.num_pos.

theorem Mathlib.Meta.Positivity.NNRat.num_ne_zero_of_ne_zero {q : ℚ≥0} : q ≠ 0 → q.num ≠ 0

Alias of the reverse direction of NNRat.num_ne_zero.

def Mathlib.Meta.Positivity.evalNNRatNum : PositivityExt

The positivity extension which identifies expressions of the form NNRat.num q, such that positivity successfully recognises q.

def Mathlib.Meta.Positivity.evalNNRatDen : PositivityExt

The positivity extension which identifies expressions of the form Rat.den a.

theorem Mathlib.Meta.Positivity.num_pos_of_pos {a : ℚ} : 0 < a → 0 < a.num

Alias of the reverse direction of Rat.num_pos.

theorem Mathlib.Meta.Positivity.num_nonneg_of_nonneg {q : ℚ} : 0 ≤ q → 0 ≤ q.num

Alias of the reverse direction of Rat.num_nonneg.

theorem Mathlib.Meta.Positivity.num_ne_zero_of_ne_zero {q : ℚ} : q ≠ 0 → q.num ≠ 0

Alias of the reverse direction of Rat.num_ne_zero.

def Mathlib.Meta.Positivity.evalRatNum : PositivityExt

The positivity extension which identifies expressions of the form Rat.num a, such that positivity successfully recognises a.

def Mathlib.Meta.Positivity.evalRatDen : PositivityExt

The positivity extension which identifies expressions of the form Rat.den a.

def Mathlib.Meta.Positivity.evalPosPart : PositivityExt

Extension for posPart. a⁺ is always nonnegative, and positive if a is.

def Mathlib.Meta.Positivity.evalNegPart : PositivityExt

Extension for negPart. a⁻ is always nonnegative.

def Mathlib.Meta.Positivity.evalMap : PositivityExt

Extension for the positivity tactic: nonnegative maps take nonnegative values.