List.nonzeroMinimum, List.minNatAbs, List.maxNatAbs

List.minNatAbs computes the minimum non-zero absolute value of a List Int. This is not generally useful outside of the implementation of the omega tactic, so we keep it in the Lean/Elab/Tactic/Omega directory (although the definitions are in the List namespace).

def List.nonzeroMinimum (xs : List Nat) : Nat

The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.

We completely characterize the function via nonzeroMinimum_eq_zero_iff and nonzeroMinimum_eq_nonzero_iff below.

Equations

• xs.nonzeroMinimum = (List.filter (fun (x : Nat) => decide (x ≠ 0)) xs).minimum?.getD 0

theorem List.minimum?_eq_some_iff' {a : Nat} {xs : List Nat} : xs.minimum? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b

@[simp]

theorem List.nonzeroMinimum_eq_zero_iff {xs : List Nat} : xs.nonzeroMinimum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

theorem List.nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) : xs.nonzeroMinimum ∈ xs

theorem List.nonzeroMinimum_pos {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum

theorem List.nonzeroMinimum_le {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a

theorem List.nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y ≠ 0) : xs.nonzeroMinimum = y ↔ y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0

theorem List.nonzeroMinimum_eq_of_nonzero {xs : List Nat} (h : xs.nonzeroMinimum ≠ 0) : ∃ (x : Nat), x ∈ xs ∧ xs.nonzeroMinimum = x

theorem List.nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} : xs.nonzeroMinimum ≤ y ↔ xs.nonzeroMinimum = 0 ∨ ∃ (x : Nat), x ∈ xs ∧ x ≤ y ∧ x ≠ 0

theorem List.nonzeroMininum_map_le_nonzeroMinimum {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → Nat) (q : β → Nat) (xs : List α) (h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)) (w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a) : (List.map q (List.map f xs)).nonzeroMinimum ≤ (List.map p xs).nonzeroMinimum

def List.minNatAbs (xs : List Int) : Nat

The minimum absolute value of a nonzero entry, or zero if all entries are zero.

We completely characterize the function via minNatAbs_eq_zero_iff and minNatAbs_eq_nonzero_iff below.

Equations

• xs.minNatAbs = (List.map Int.natAbs xs).nonzeroMinimum

@[simp]

theorem List.minNatAbs_eq_zero_iff {xs : List Int} : xs.minNatAbs = 0 ↔ ∀ (y : Int), y ∈ xs → y = 0

theorem List.minNatAbs_eq_nonzero_iff {z : Nat} (xs : List Int) (w : z ≠ 0) : xs.minNatAbs = z ↔ (∃ (y : Int), y ∈ xs ∧ y.natAbs = z) ∧ ∀ (y : Int), y ∈ xs → z ≤ y.natAbs ∨ y = 0

@[simp]

theorem List.minNatAbs_nil : [].minNatAbs = 0

def List.maxNatAbs (xs : List Int) : Nat

The maximum absolute value in a list of integers.

Equations

• xs.maxNatAbs = (List.map Int.natAbs xs).maximum?.getD 0