The ultrametric inequality for quotients and differences

In an ultrametric seminormed group, ‖x / y‖ ≤ max ‖x‖ ‖y‖; additively, ‖x - y‖ ≤ max ‖x‖ ‖y‖, and likewise for ‖·‖₊. These are the companions of Mathlib's IsUltrametricDist.norm_mul_le_max and IsUltrametricDist.norm_add_le_max. Measured from a common point y, the triangle inequality reads ‖x - z‖ ≤ max ‖x - y‖ ‖z - y‖. If ‖x - y‖ < ‖x‖ then ‖x‖ = ‖y‖: an element and a strictly smaller perturbation of it have the same norm, and if x and y - x both have norm at most C, so does y.

A separable ultrametric additive group with a strictly decreasing sequence of norms ‖cₙ‖ bounded away from 0 is not spherically complete: there are decreasing closed balls of radii ‖cₙ‖ with empty intersection (IsUltrametricDist.exists_antitone_closedBall_iInter_eq_empty). Enumerate a dense sequence xₙ and choose the (n + 1)-st ball to avoid xₙ, keeping the centre when it is already far from xₙ and moving it by cₙ otherwise. A common point b of the balls would have all of them containing the ball of radius inf ‖cₙ‖ > 0 about b, hence some xₙ. For ℂ_p this is the classical construction of a decreasing sequence of discs without a common point; see A. M. Robert, A Course in p-adic Analysis, Graduate Texts in Mathematics 198, Springer, 2000, Chapter 3.

theorem IsUltrametricDist.norm_div_le_max {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y : S) : ‖x / y‖ ≤ max ‖x‖ ‖y‖

The ultrametric inequality for a quotient: ‖x / y‖ ≤ max ‖x‖ ‖y‖.

theorem IsUltrametricDist.norm_sub_le_max {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y : S) : ‖x - y‖ ≤ max ‖x‖ ‖y‖

The ultrametric inequality for a difference: ‖x - y‖ ≤ max ‖x‖ ‖y‖.

theorem IsUltrametricDist.nnnorm_div_le_max {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y : S) : ‖x / y‖₊ ≤ max ‖x‖₊ ‖y‖₊

The ultrametric inequality for a quotient: ‖x / y‖₊ ≤ max ‖x‖₊ ‖y‖₊.

theorem IsUltrametricDist.nnnorm_sub_le_max {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y : S) : ‖x - y‖₊ ≤ max ‖x‖₊ ‖y‖₊

The ultrametric inequality for a difference: ‖x - y‖₊ ≤ max ‖x‖₊ ‖y‖₊.

theorem IsUltrametricDist.norm_eq_of_norm_div_lt_left {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x / y‖ < ‖x‖) : ‖x‖ = ‖y‖

In an ultrametric group, if ‖x / y‖ < ‖x‖ then x and y have the same norm.

theorem IsUltrametricDist.norm_eq_of_norm_sub_lt_left {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x - y‖ < ‖x‖) : ‖x‖ = ‖y‖

In an ultrametric additive group, if ‖x - y‖ < ‖x‖ then x and y have the same norm.

theorem IsUltrametricDist.norm_le_of_norm_div_le {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] {x y : S} {C : ℝ} (hx : ‖x‖ ≤ C) (h : ‖y / x‖ ≤ C) : ‖y‖ ≤ C

In an ultrametric group, if x and the quotient y / x both have norm at most C, so does y.

theorem IsUltrametricDist.norm_le_of_norm_sub_le {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] {x y : S} {C : ℝ} (hx : ‖x‖ ≤ C) (h : ‖y - x‖ ≤ C) : ‖y‖ ≤ C

In an ultrametric additive group, if x and the difference y - x both have norm at most C, so does y.

theorem IsUltrametricDist.norm_div_le_max_norm_div {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y z : S) : ‖x / z‖ ≤ max ‖x / y‖ ‖z / y‖

The ultrametric triangle inequality for quotients, measured from a common point y: ‖x / z‖ ≤ max ‖x / y‖ ‖z / y‖.

theorem IsUltrametricDist.norm_sub_le_max_norm_sub {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y z : S) : ‖x - z‖ ≤ max ‖x - y‖ ‖z - y‖

The ultrametric triangle inequality for differences, measured from a common point y: ‖x - z‖ ≤ max ‖x - y‖ ‖z - y‖.

theorem IsUltrametricDist.exists_antitone_closedBall_iInter_eq_empty {E : Type u_2} [SeminormedAddCommGroup E] [IsUltrametricDist E] [TopologicalSpace.SeparableSpace E] {c : ℕ → E} (hc : StrictAnti fun (n : ℕ) => ‖c n‖) {ρ : ℝ} (hρ : 0 < ρ) (hcρ : ∀ (n : ℕ), ρ ≤ ‖c n‖) (a₀ : E) : ∃ (a : ℕ → E), a 0 = a₀ ∧ (Antitone fun (n : ℕ) => Metric.closedBall (a n) ‖c n‖) ∧ ⋂ (n : ℕ), Metric.closedBall (a n) ‖c n‖ = ∅

A separable ultrametric group is not spherically complete once its norms take a strictly decreasing sequence of values ‖cₙ‖ bounded below by some ρ > 0: there are decreasing closed balls of radii ‖cₙ‖, starting at any centre a₀, with empty intersection.