Sums under a weakened triangle inequality

An absolute value satisfies v (a + b) ≤ c * max (v a) (v b) with c = 2, and with c = 1 when it is nonarchimedean. Iterating this inequality bounds a sum of n terms of size at most T by c ^ n * T (AbsoluteValue.apply_sum_le_pow_mul). Unlike the triangle inequality, which gives n * T, the bound specializes to T itself in the nonarchimedean case.

The same inequality bounds one step of elimination with partial pivoting: subtracting from a the multiple p / q * b of a pivot column, whose pivot q dominates b relative to the row weights, costs only the factor c (AbsoluteValue.apply_sub_div_mul_le), and a maximizing pivot exists (AbsoluteValue.exists_pos_forall_apply_div_le).

theorem AbsoluteValue.apply_natCast_mul_le {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] (v : AbsoluteValue R S) (n : ℕ) (x : R) : v (↑n * x) ≤ ↑n * v x

The triangle inequality gives v (n * x) ≤ n * v x for a natural number n, without using v 1 = 1 (so for an absolute value valued in any ordered semiring).

theorem AbsoluteValue.apply_sum_le_pow_mul {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [LinearOrder S] [IsOrderedRing S] {v : AbsoluteValue R S} {c : S} (hc : 1 ≤ c) (hv : ∀ (a b : R), v (a + b) ≤ c * max (v a) (v b)) {ι : Type u_3} (s : Finset ι) (f : ι → R) {T : S} (hT : 0 ≤ T) (hf : ∀ i ∈ s, v (f i) ≤ T) : v (∑ i ∈ s, f i) ≤ c ^ s.card * T

A sum of card s terms of size at most T has size at most c ^ card s * T, for an absolute value satisfying v (a + b) ≤ c * max (v a) (v b) with 1 ≤ c.

theorem AbsoluteValue.apply_sub_div_mul_le {K : Type u_3} {F : Type u_4} [DivisionRing K] [Field F] [LinearOrder F] [IsStrictOrderedRing F] {v : AbsoluteValue K F} {c : F} (hc : 0 ≤ c) (hv : ∀ (a b : K), v (a + b) ≤ c * max (v a) (v b)) {a b p q : K} {s t M : F} (hs : 0 < s) (ht : 0 < t) (hq : 0 < v q) (ha : v a ≤ s * M) (hp : v p ≤ t * M) (hb : v b / s ≤ v q / t) : v (a - p / q * b) ≤ c * (s * M)

One elimination step: if the pivot q maximizes v (·) / s in its column, then subtracting p / q times that column from a column bounded by M (in units of the row weights s, t) keeps it bounded by c * M, for an absolute value satisfying v (a + b) ≤ c * max (v a) (v b).

theorem AbsoluteValue.apply_add_le_two_mul_max {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [LinearOrder S] [IsOrderedRing S] (v : AbsoluteValue R S) (a b : R) : v (a + b) ≤ 2 * max (v a) (v b)

The growth factor of one addition: v (a + b) ≤ 2 * max (v a) (v b). At a nonarchimedean absolute value the factor 2 can be replaced by 1 (IsNonarchimedean).

theorem AbsoluteValue.exists_pos_forall_apply_div_le {R : Type u_1} [Semiring R] {ρ : Type u_3} {T : Type u_4} [Finite ρ] [Semifield T] [LinearOrder T] [IsStrictOrderedRing T] (v : AbsoluteValue R T) {f : ρ → R} (hf : ∃ (r : ρ), f r ≠ 0) {ν : ρ → T} (hν : ∀ (r : ρ), 0 < ν r) : ∃ (r₀ : ρ), 0 < v (f r₀) ∧ ∀ (r : ρ), v (f r) / ν r ≤ v (f r₀) / ν r₀

Partial pivoting at one place: a nonzero family of elements of a semiring has an index r₀ maximizing v (f r) / ν r for positive weights ν, and the value there is positive.