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 Std/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

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

@[simp]

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

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

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

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

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

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

theorem List.nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} : List.nonzeroMinimum xs ≤ y ↔ List.nonzeroMinimum xs = 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.nonzeroMinimum (List.map q (List.map f xs)) ≤ List.nonzeroMinimum (List.map p xs)

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

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

@[simp]

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

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

@[simp]

theorem List.minNatAbs_nil : List.minNatAbs [] = 0

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

The maximum absolute value in a list of integers.

Equations

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