The closed unit ball and products of elements close to one in ultrametric normed rings

An ultrametric seminormed ring is a nonarchimedean topological ring: its open balls about zero are open additive subgroups. In an ultrametric seminormed ring with ‖1‖ = 1, the closed unit ball is an open subring. In an ultrametric normed ring, a finite product of elements each within ε ≤ 1 of 1 is again within ε of 1. A series ∑_{n ≥ 1} f(qⁿ w) of terms bounded by their arguments is bounded by its first argument q w, and it depends on w in a ‖q‖-Lipschitz way when its terms are 1-Lipschitz. The rational functions t / (1 - t)², t / (1 - t)³ and t² / (1 - t)³ are Lipschitz on the open unit ball of an ultrametric field.

Integer casts have norm at most ‖1‖, without requiring the seminorm to be normalized. When ‖1‖ = 1, arbitrarily large natural numbers have norm exactly one. Since the forward differences of a monomial are divisible by k!, their norms carry the factor ‖k!‖.

Main results

• IsUltrametricDist.exists_lt_norm_natCast_eq_one: arbitrarily large natural numbers have norm one in an ultrametric seminormed ring with ‖1‖ = 1.
• IsUltrametricDist.nonarchimedeanRing: an ultrametric seminormed ring is a nonarchimedean ring.
• Subring.unitClosedBall: the closed unit ball of an ultrametric seminormed ring with ‖1‖ = 1, an open subring.
• TauCeti.norm_one_sub_of_norm_lt_one: subtracting an element of norm less than one from one leaves the norm equal to one; TauCeti.norm_eq_one_of_norm_one_sub_lt_one: an element within less than one of one has norm one; TauCeti.norm_div_one_sub_pow: dividing by a power of such a 1 - w does not change norms.
• TauCeti.norm_div_one_sub_cube_sub_div_one_sub_cube_le and TauCeti.norm_sq_div_one_sub_cube_sub_sq_div_one_sub_cube_le_max_mul: on the open unit ball, t ↦ t / (1 - t)³ is 1-Lipschitz and t ↦ t² / (1 - t)³ is Lipschitz with constant the larger of the two norms.
• TauCeti.norm_tsum_le_norm_mul: a one-sided series ∑_{n ≥ 1} f(qⁿ w) whose terms are bounded by their arguments has norm at most ‖q w‖; TauCeti.norm_tsum_sub_tsum_le_norm_mul: if the terms are 1-Lipschitz, two such series differ by at most ‖q (w - w')‖; TauCeti.norm_tsum_sub_tsum_add_tsum_sub_tsum_le: a series at u and a series at u⁻¹ of 1-Lipschitz terms together depend on u in a ‖q‖-Lipschitz way on the unit circle.
• TauCeti.norm_div_one_sub_sq_sub_div_one_sub_sq_le: the map t ↦ t / (1 - t)² is 1-Lipschitz on the open unit ball of an ultrametric field; TauCeti.norm_sub_le_of_eq_mul_div is the estimate behind it.
• TauCeti.norm_one_sub_cube_div_sub_one_sub_cube_div_le: the map v ↦ (1 - v)³ / v is 1-Lipschitz on the unit circle of an ultrametric field.
• TauCeti.one_le_norm_one_sub_of_norm_ne_one: subtracting an element whose norm is not one from one gives norm at least one.
• TauCeti.norm_mul_sub_one_lt and TauCeti.norm_prod_sub_one_lt
• TauCeti.norm_pow_sub_one_le_norm_sub_one: a power of an element x of norm at most one is no farther from 1 than x.
• TauCeti.norm_prod_sub_prod_le: a uniform perturbation bound for finite products.
• TauCeti.norm_fwdDiff_iter_pow_mul_pow_le: for ‖x‖, ‖h‖ ≤ c, the k-th forward difference of y ↦ yᵐ with step h at x satisfies ‖Δₕᵏ (y ↦ yᵐ)(x)‖ cᵏ ≤ ‖k!‖ ‖h‖ᵏ cᵐ.

theorem IsUltrametricDist.norm_intCast_le_norm_one {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] (z : ℤ) : ‖↑z‖ ≤ ‖1‖

Integer casts in an ultrametric seminormed ring have norm at most the norm of one.

theorem IsUltrametricDist.exists_lt_norm_natCast_eq_one (R : Type u_1) [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (N : ℕ) : ∃ (m : ℕ), N < m ∧ ‖↑m‖ = 1

In an ultrametric seminormed ring with ‖1‖ = 1, arbitrarily large natural numbers have norm one: of two consecutive natural numbers, one has norm one, since their difference does.

instance IsUltrametricDist.nonarchimedeanRing {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] : NonarchimedeanRing R

An ultrametric seminormed ring is a nonarchimedean ring. This is the ring form of Mathlib's IsUltrametricDist.nonarchimedeanAddGroup: every neighbourhood of zero contains an open additive subgroup, namely a small open ball.

def Subring.unitClosedBall (R : Type u_1) [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] : Subring R

The closed unit ball of an ultrametric seminormed ring with ‖1‖ = 1 is a subring: it is the submonoid Submonoid.unitClosedBall and the open additive subgroup IsUltrametricDist.closedBall_openAddSubgroup.

@[simp]

theorem Subring.mem_unitClosedBall {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] {x : R} : x ∈ unitClosedBall R ↔ ‖x‖ ≤ 1

An element lies in the closed unit ball exactly when its norm is at most one.

@[simp]

theorem Subring.coe_unitClosedBall (R : Type u_1) [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] : ↑(unitClosedBall R) = Metric.closedBall 0 1

The carrier of Subring.unitClosedBall R is Metric.closedBall 0 1.

theorem Subring.isOpen_unitClosedBall (R : Type u_1) [SeminormedRing R] [IsUltrametricDist R] [NormOneClass R] : IsOpen ↑(unitClosedBall R)

The closed unit ball of an ultrametric seminormed ring is open.

@[simp]

theorem TauCeti.norm_one_sub_of_norm_lt_one {R : Type u_1} [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] {x : R} (hx : ‖x‖ < 1) : ‖1 - x‖ = 1

An element strictly smaller than one does not change the norm of one when subtracted.

theorem TauCeti.norm_eq_one_of_norm_one_sub_lt_one {R : Type u_1} [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] {x : R} (hx : ‖1 - x‖ < 1) : ‖x‖ = 1

An element at distance less than one from one has norm one.

theorem TauCeti.one_le_norm_one_sub_of_norm_ne_one {R : Type u_1} [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] {x : R} (hx : ‖x‖ ≠ 1) : 1 ≤ ‖1 - x‖

Subtracting an element whose norm is not one from one gives norm at least one.

theorem TauCeti.norm_div_one_sub_pow {K : Type u_1} [NormedDivisionRing K] [IsUltrametricDist K] (z : K) {w : K} (hw : ‖w‖ < 1) (k : ℕ) : ‖z / (1 - w) ^ k‖ = ‖z‖

Dividing by a power of 1 - w with ‖w‖ < 1 does not change norms in an ultrametric normed division ring.

theorem TauCeti.norm_div_one_sub_cube_sub_div_one_sub_cube_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] {t t' : K} (ht : ‖t‖ < 1) (ht' : ‖t'‖ < 1) : ‖t / (1 - t) ^ 3 - t' / (1 - t') ^ 3‖ ≤ ‖t - t'‖

The map t ↦ t / (1 - t)³ is 1-Lipschitz on the open unit ball of an ultrametric field.

theorem TauCeti.norm_sq_div_one_sub_cube_sub_sq_div_one_sub_cube_le_max_mul {K : Type u_1} [NormedField K] [IsUltrametricDist K] {t t' : K} (ht : ‖t‖ < 1) (ht' : ‖t'‖ < 1) : ‖t ^ 2 / (1 - t) ^ 3 - t' ^ 2 / (1 - t') ^ 3‖ ≤ max ‖t‖ ‖t'‖ * ‖t - t'‖

On the open unit ball of an ultrametric field, the map t ↦ t² / (1 - t)³ is Lipschitz with constant max ‖t‖ ‖t'‖ between t and t', so it contracts near zero.

theorem TauCeti.norm_tsum_le_norm_mul {R : Type u_1} {E : Type u_2} [SeminormedRing R] [SeminormedAddCommGroup E] [IsUltrametricDist E] (f : R → E) (hf : ∀ (w : R), ‖w‖ < 1 → ‖f w‖ ≤ ‖w‖) {q w : R} (hq : ‖q‖ ≤ 1) (hw : ‖q * w‖ < 1) : ‖∑' (n : ℕ), f (q ^ (n + 1) * w)‖ ≤ ‖q * w‖

A one-sided series ∑_{n ≥ 1} f(qⁿ w) with values in an ultrametric group, whose terms are bounded by their arguments, has norm at most ‖q w‖ when ‖q‖ ≤ 1 and ‖q w‖ < 1.

theorem TauCeti.norm_tsum_sub_tsum_le_norm_mul {R : Type u_1} {E : Type u_2} [SeminormedRing R] [NormedAddCommGroup E] [IsUltrametricDist E] (f : R → E) (hf : ∀ (t t' : R), ‖t‖ < 1 → ‖t'‖ < 1 → ‖f t - f t'‖ ≤ ‖t - t'‖) {q w w' : R} (hq : ‖q‖ ≤ 1) (hw : ‖q * w‖ < 1) (hw' : ‖q * w'‖ < 1) (hs : Summable fun (n : ℕ) => f (q ^ (n + 1) * w)) (hs' : Summable fun (n : ℕ) => f (q ^ (n + 1) * w')) : ‖∑' (n : ℕ), f (q ^ (n + 1) * w) - ∑' (n : ℕ), f (q ^ (n + 1) * w')‖ ≤ ‖q * (w - w')‖

Two convergent one-sided series ∑_{n ≥ 1} f(qⁿ w) and ∑_{n ≥ 1} f(qⁿ w') with values in an ultrametric group, whose terms are 1-Lipschitz on the open unit ball, differ by at most ‖q (w - w')‖ when ‖q‖ ≤ 1 and ‖q w‖, ‖q w'‖ < 1.

theorem TauCeti.norm_tsum_sub_tsum_add_tsum_sub_tsum_le {K : Type u_1} {E : Type u_2} [NormedField K] [NormedAddCommGroup E] [IsUltrametricDist E] {q u u' : K} (hq : ‖q‖ < 1) (hu : ‖u‖ = 1) (hu' : ‖u'‖ = 1) (f g : K → E) (hf : ∀ (t t' : K), ‖t‖ < 1 → ‖t'‖ < 1 → ‖f t - f t'‖ ≤ ‖t - t'‖) (hg : ∀ (t t' : K), ‖t‖ < 1 → ‖t'‖ < 1 → ‖g t - g t'‖ ≤ ‖t - t'‖) (hfs : Summable fun (n : ℕ) => f (q ^ (n + 1) * u)) (hfs' : Summable fun (n : ℕ) => f (q ^ (n + 1) * u')) (hgs : Summable fun (n : ℕ) => g (q ^ (n + 1) * u⁻¹)) (hgs' : Summable fun (n : ℕ) => g (q ^ (n + 1) * u'⁻¹)) : ‖∑' (n : ℕ), f (q ^ (n + 1) * u) - ∑' (n : ℕ), f (q ^ (n + 1) * u') + (∑' (n : ℕ), g (q ^ (n + 1) * u⁻¹) - ∑' (n : ℕ), g (q ^ (n + 1) * u'⁻¹))‖ ≤ ‖q‖ * ‖u - u'‖

A one-sided series ∑_{n ≥ 1} f(qⁿ u) at u and one ∑_{n ≥ 1} g(qⁿ u⁻¹) at u⁻¹, with values in an ultrametric group, together depend on u in a ‖q‖-Lipschitz way on the unit circle when their terms are 1-Lipschitz on the open unit ball and ‖q‖ < 1. Only the values need to be ultrametric.

theorem TauCeti.norm_sub_le_of_eq_mul_div {K : Type u_1} [NormedField K] [IsUltrametricDist K] {t t' a a' P : K} (ht : ‖t‖ < 1) (ht' : ‖t'‖ < 1) {k : ℕ} (h : a - a' = (t - t') * P / ((1 - t) ^ k * (1 - t') ^ k)) (hP : ‖P‖ ≤ 1) : ‖a - a'‖ ≤ ‖t - t'‖

A difference of the form (t - t') P / ((1 - t)ᵏ (1 - t')ᵏ) with ‖t‖, ‖t'‖ < 1 and ‖P‖ ≤ 1 has norm at most ‖t - t'‖.

theorem TauCeti.norm_div_one_sub_sq_sub_div_one_sub_sq_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] {t t' : K} (ht : ‖t‖ < 1) (ht' : ‖t'‖ < 1) : ‖t / (1 - t) ^ 2 - t' / (1 - t') ^ 2‖ ≤ ‖t - t'‖

The map t ↦ t / (1 - t)² is 1-Lipschitz on the open unit ball of an ultrametric field.

theorem TauCeti.norm_one_sub_cube_div_sub_one_sub_cube_div_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] {v w : K} (hv : ‖v‖ = 1) (hw : ‖w‖ = 1) : ‖(1 - v) ^ 3 / v - (1 - w) ^ 3 / w‖ ≤ ‖v - w‖

The map v ↦ (1 - v)³ / v is 1-Lipschitz on the unit circle of an ultrametric field.

theorem TauCeti.norm_mul_sub_one_lt {R : Type u_1} [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] {a b : R} {ε : ℝ} (hε : ε ≤ 1) (ha : ‖a - 1‖ < ε) (hb : ‖b - 1‖ < ε) : ‖a * b - 1‖ < ε

In an ultrametric normed ring, if a and b are both within ε ≤ 1 of 1, so is a * b.

theorem TauCeti.norm_pow_sub_one_le_norm_sub_one {R : Type u_1} [SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] {x : R} (hx : ‖x‖ ≤ 1) (n : ℕ) : ‖x ^ n - 1‖ ≤ ‖x - 1‖

In an ultrametric seminormed ring with ‖1‖ = 1, a power of an element x of norm at most one is no farther from 1 than x is: ‖x ^ n - 1‖ ≤ ‖x - 1‖.

theorem TauCeti.norm_prod_sub_one_lt {ι : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] (s : Finset ι) (f : ι → R) {ε : ℝ} (hε0 : 0 < ε) (hε : ε ≤ 1) (hf : ∀ i ∈ s, ‖f i - 1‖ < ε) : ‖∏ i ∈ s, f i - 1‖ < ε

In an ultrametric normed commutative ring, a finite product of elements each within ε ≤ 1 of 1 is again within ε of 1 (for 0 < ε).

theorem TauCeti.norm_prod_sub_prod_le {ι : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {s : Finset ι} {f g : ι → R} {M ε : ℝ} (hM : 0 ≤ M) (hε : 0 ≤ ε) (hf : ∀ i ∈ s, ‖f i‖ ≤ M) (hg : ∀ i ∈ s, ‖g i‖ ≤ M) (hfg : ∀ i ∈ s, ‖f i - g i‖ ≤ ε) : ‖∏ i ∈ s, f i - ∏ i ∈ s, g i‖ ≤ ε * M ^ (s.card - 1)

If two finite families are bounded by M and differ by at most ε in each coordinate, their products differ by at most ε * M ^ (s.card - 1). The exponent uses natural subtraction, so the statement includes the empty product and M = 0.

theorem TauCeti.norm_fwdDiff_iter_pow_mul_pow_le {A : Type u_1} [SeminormedCommRing A] [NormOneClass A] [IsUltrametricDist A] {c : ℝ} {h x : A} (hh : ‖h‖ ≤ c) (hx : ‖x‖ ≤ c) (k m : ℕ) : ‖(fwdDiff h)^[k] (fun (y : A) => y ^ m) x‖ * c ^ k ≤ ‖↑k.factorial‖ * ‖h‖ ^ k * c ^ m

Forward differences of powers. In an ultrametric seminormed commutative ring with ‖1‖ = 1, for a point x and a step h with ‖x‖ ≤ c and ‖h‖ ≤ c, ‖Δₕᵏ (y ↦ yᵐ)(x)‖ cᵏ ≤ ‖k!‖ ‖h‖ᵏ cᵐ.