Maximum absolute value of a tuple of integers

def maxAbs {n : ℕ} (a : Fin n → ℤ) : ℕ

The maximum absolute value of a tuple of integers (0 if empty).

Equations

• maxAbs a = Finset.univ.sup fun (i : Fin n) => (a i).natAbs

theorem maxAbs_zero {a : Fin 0 → ℤ} : maxAbs a = 0

theorem maxAbs_one {a : Fin 1 → ℤ} : maxAbs a = (a 0).natAbs

theorem maxAbs_eq_foldr {n : ℕ} {a : Fin n → ℤ} : maxAbs a = List.foldr max 0 (List.ofFn fun (i : Fin n) => (a i).natAbs)

theorem maxAbs_eq_of_forall_le {n : ℕ} {a : Fin n → ℤ} {i : Fin n} (hi : ∀ (j : Fin n), (a j).natAbs ≤ (a i).natAbs) : maxAbs a = (a i).natAbs