Magnitude bounds on integer powers and list sums

Bounds on the absolute value Int.natAbs of powers of integers, and bounds on the absolute value of sums and prefix sums of lists of integers bounded termwise.

Main results

• Int.natAbs_pow_le: (z ^ q).natAbs ≤ H ^ M when z.natAbs ≤ H and q ≤ M.
• List.natAbs_sum_le_length_mul: l.sum.natAbs ≤ l.length * C when every element of l is bounded by C.
• List.natAbs_sum_take_le_length_mul: every prefix sum of l is bounded by l.length * C.
• List.natAbs_sum_take_le_of_length_le: prefix sums are bounded by m * C when l.length ≤ m.
• List.natAbs_getD_le_of_forall: getD with default 0 preserves elementwise natAbs bounds.

theorem Int.natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ} (hq : q ≤ M) : (z ^ q).natAbs ≤ H ^ M

A power of an integer is bounded in magnitude by the corresponding power of a bound on the base.

theorem List.natAbs_sum_le_length_mul {l : List ℤ} {C : ℕ} (h : ∀ (x : ℤ), x ∈ l → x.natAbs ≤ C) : l.sum.natAbs ≤ l.length * C

The magnitude of a sum of integers is at most the length times a termwise bound.

theorem List.natAbs_sum_take_le_length_mul {l : List ℤ} {C : ℕ} (h : ∀ (x : ℤ), x ∈ l → x.natAbs ≤ C) (m : ℕ) : (take m l).sum.natAbs ≤ l.length * C

Every prefix sum of a list is bounded by its length times a bound on its entries.

theorem List.natAbs_sum_take_le_of_length_le {l : List ℤ} {C m : ℕ} (hl : l.length ≤ m) (h : ∀ (x : ℤ), x ∈ l → x.natAbs ≤ C) (k : ℕ) : (take k l).sum.natAbs ≤ m * C

Every prefix sum and the sum of a list of terms bounded by C are bounded by m * C, where m bounds the length.

theorem List.natAbs_getD_le_of_forall {l : List ℤ} {B : ℕ} (hl : ∀ (x : ℤ), x ∈ l → x.natAbs ≤ B) (i : ℕ) : (l.getD i 0).natAbs ≤ B

Looking up l.getD i 0 preserves any uniform bound on Int.natAbs of elements of l.