Elementary inequalities in seminormed rings

This file records elementary consequences of the submultiplicativity of the norm, and an estimate for ‖w - 1‖ with ‖w‖ = 1 when the norm is multiplicative.

theorem TauCeti.norm_mul_lt_one {K : Type u_1} [NonUnitalSeminormedRing K] (u v : K) (hu : ‖u‖ < 1) (hv : ‖v‖ < 1) : ‖u * v‖ < 1

A product of two elements in the open unit ball again belongs to the open unit ball.

theorem TauCeti.norm_pow_succ_mul_pow_lt_one {K : Type u_1} [SeminormedRing K] (u v : K) (hu : ‖u‖ < 1) (hv : ‖v‖ ≤ 1) (n : ℕ) : ‖u ^ (n + 1) * v ^ n‖ < 1

Consecutive powers stay in the open unit ball when the first factor is strictly inside and the second factor is in the closed unit ball.

theorem TauCeti.norm_pow_lt_one {R : Type u_1} [SeminormedRing R] {q : R} (hq : ‖q‖ < 1) {n : ℕ} (hn : n ≠ 0) : ‖q ^ n‖ < 1

For ‖q‖ < 1 also ‖qⁿ‖ < 1 for every n ≠ 0.

theorem TauCeti.norm_pow_succ_mul_le {R : Type u_1} [SeminormedRing R] {q : R} (hq : ‖q‖ ≤ 1) (w : R) (n : ℕ) : ‖q ^ (n + 1) * w‖ ≤ ‖q * w‖

Multiplying by further powers of an element of norm at most one does not increase the norm: ‖qⁿ⁺¹ w‖ ≤ ‖q w‖ when ‖q‖ ≤ 1.

theorem TauCeti.norm_pow_le_max_mul {R : Type u_1} [SeminormedRing R] (x : R) (n : ℕ) : ‖x ^ n‖ ≤ max ‖1‖ 1 * ‖x‖ ^ n

Without the normalisation ‖1‖ = 1, powers are still bounded by ‖xⁿ‖ ≤ max ‖1‖ 1 * ‖x‖ⁿ, including the power x⁰ = 1.

theorem TauCeti.norm_mul_pow_le {R : Type u_1} [SeminormedRing R] (x y : R) (n : ℕ) : ‖x * y ^ n‖ ≤ ‖x‖ * ‖y‖ ^ n

Without the normalisation ‖1‖ = 1, a product with a power still satisfies ‖x * yⁿ‖ ≤ ‖x‖ * ‖y‖ⁿ, including the case n = 0, where x * y⁰ = x.

theorem TauCeti.norm_sub_one_le_norm_sub_one_mul_add {R : Type u_1} [SeminormedRing R] [NormMulClass R] [NormOneClass R] {w a r : R} (hw : ‖w‖ = 1) (hr : ‖r‖ ≤ 1) : ‖w - 1‖ ≤ ‖(w - 1) * a‖ + 2 * ‖a - r‖ + 2 * (1 - ‖r‖)

For a multiplicative norm with ‖1‖ = 1, an element w of norm one and r of norm at most one, ‖w - 1‖ ≤ ‖(w - 1) a‖ + 2 ‖a - r‖ + 2 (1 - ‖r‖) for every a. So w - 1 is controlled by (w - 1) a wherever a is close to some r of norm close to one.