Rounding norms up to the powers of a constant

Fix 0 < c < 1. Every real number x has a least upper bound in the discrete set c ^ ℤ ∪ {0}: for x > 0 it is the unique power c ^ n with c ^ (n + 1) < x ≤ c ^ n, and for x ≤ 0 it is 0. We call this value TauCeti.zpowCeil c x. It is monotone, it lies within the factor c of x (x ≤ zpowCeil c x and c * zpowCeil c x < x for x > 0), it commutes with multiplication by powers of c, and it is submultiplicative on nonnegative numbers.

Applied to the norm of an ultrametric seminormed group M, rounding produces a new ultrametric seminorm TauCeti.zpowCeilAddGroupSeminorm with values in c ^ ℤ ∪ {0}. It is bounded-equivalent to the original norm, c * zpowCeil c ‖m‖ ≤ ‖m‖ ≤ zpowCeil c ‖m‖, and it vanishes exactly where the norm does. For a contractive scalar action of a seminormed ring R, rounding gives zpowCeil c ‖a • m‖ ≤ zpowCeil c ‖a‖ * zpowCeil c ‖m‖. Thus the rounded norm is again a contractive module norm when the norm of R already takes values in c ^ ℤ ∪ {0}, and in general it still scales exactly under every scalar a with ‖a • m‖ = c ^ n * ‖m‖, such as a multiplicative pseudo-uniformiser of norm c.

Rounding is the standard device for replacing a Banach module over a discretely valued ring by one whose norm takes values in the value group of the ring. Strict inequalities against powers of c then become non-strict ones (zpowCeil_lt_zpow_iff), which is what makes the open unit ball of the rounded norm a principal multiple of the closed unit ball. This is the input to Serre's reduction of orthonormalisability to freeness of a residue module.

zpowCeilNormedAddCommGroup installs this rounded norm while retaining the original uniformity and topology definitionally. Thus completeness and continuous linear maps are unchanged. Ultrametricity and contractive scalar actions with discrete scalar norms can be installed explicitly using isUltrametricDist_zpowCeilNormedAddCommGroup and isBoundedSMul_zpowCeilNormedAddCommGroup.

Main definitions

• TauCeti.zpowCeil c x: the least element of c ^ ℤ ∪ {0} that is at least x.
• TauCeti.zpowCeilAddGroupSeminorm hc₀ hc₁ M: the norm of an ultrametric seminormed group rounded up to c ^ ℤ ∪ {0}.
• TauCeti.zpowCeilAddGroupNorm hc₀ hc₁ M: the same construction on a normed group, as a norm.

Main results

• TauCeti.zpowCeil_le_iff: zpowCeil c x ≤ y ↔ x ≤ y whenever y lies in c ^ ℤ ∪ {0}.
• TauCeti.zpowCeil_eq_zpow_iff: zpowCeil c x = c ^ n ↔ c ^ (n + 1) < x ∧ x ≤ c ^ n.
• TauCeti.le_zpowCeil and TauCeti.mul_zpowCeil_lt: x ≤ zpowCeil c x and, for x > 0, c * zpowCeil c x < x.
• TauCeti.zpowCeil_zpow_mul: zpowCeil c (c ^ n * x) = c ^ n * zpowCeil c x.
• TauCeti.zpowCeil_norm_smul_le: rounding is compatible with contractive scalar actions.
• TauCeti.isNonarchimedean_zpowCeilAddGroupSeminorm: the rounded seminorm is ultrametric.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §1.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

noncomputable def TauCeti.zpowCeil (c x : ℝ) : ℝ

The least element of c ^ ℤ ∪ {0} that is at least x, for 0 < c < 1: the power c ^ n with c ^ (n + 1) < x ≤ c ^ n when x > 0, and 0 when x ≤ 0.

theorem TauCeti.zpowCeil_of_pos {c x : ℝ} (hx : 0 < x) : zpowCeil c x = c ^ ⌊Real.logb c x⌋

A positive number is rounded to c ^ ⌊logb c x⌋.

theorem TauCeti.zpowCeil_of_nonpos {c x : ℝ} (hx : x ≤ 0) : zpowCeil c x = 0

A nonpositive number is rounded to 0.

@[simp]

theorem TauCeti.zpowCeil_zero {c : ℝ} : zpowCeil c 0 = 0

Zero is rounded to 0.

theorem TauCeti.zpowCeil_nonneg {c : ℝ} (hc₀ : 0 ≤ c) (x : ℝ) : 0 ≤ zpowCeil c x

Rounded values are nonnegative.

theorem TauCeti.zpowCeil_pos_iff {c x : ℝ} (hc₀ : 0 < c) : 0 < zpowCeil c x ↔ 0 < x

The rounding of x is positive exactly when x is.

theorem TauCeti.zpowCeil_eq_zero_iff {c x : ℝ} (hc₀ : 0 < c) : zpowCeil c x = 0 ↔ x ≤ 0

The rounding of x vanishes exactly when x ≤ 0.

theorem TauCeti.exists_zpowCeil_eq_zpow {c x : ℝ} (hx : 0 < x) : ∃ (n : ℤ), zpowCeil c x = c ^ n

A positive number is rounded to an integer power of c.

theorem TauCeti.existsUnique_zpow_mul_mem_Ioc {r a : ℝ} (hr0 : 0 < r) (hr1 : r < 1) (ha : 0 < a) : ∃! n : ℤ, r ^ n * a ∈ Set.Ioc r 1

The shell, for a positive real number: for a real base 0 < r < 1, every a > 0 has a unique rescaling r ^ n * a, n ∈ ℤ, with r < r ^ n * a ≤ 1.

theorem TauCeti.le_zpowCeil {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (x : ℝ) : x ≤ zpowCeil c x

Rounding up dominates: x ≤ zpowCeil c x.

theorem TauCeti.mul_zpowCeil_lt {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hx : 0 < x) : c * zpowCeil c x < x

Rounding up loses less than the factor c: c * zpowCeil c x < x for x > 0.

theorem TauCeti.mul_zpowCeil_le {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hx : 0 ≤ x) : c * zpowCeil c x ≤ x

The non-strict form of mul_zpowCeil_lt, valid for every x ≥ 0.

theorem TauCeti.zpowCeil_eq_zpow_iff {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (n : ℤ) : zpowCeil c x = c ^ n ↔ c ^ (n + 1) < x ∧ x ≤ c ^ n

zpowCeil c x is the integer power c ^ n exactly when x lies in the half-open interval (c ^ (n + 1), c ^ n].

@[simp]

theorem TauCeti.zpowCeil_zpow {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (n : ℤ) : zpowCeil c (c ^ n) = c ^ n

An integer power of c is its own rounding.

@[simp]

theorem TauCeti.zpowCeil_one {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) : zpowCeil c 1 = 1

One is its own rounding.

@[simp]

theorem TauCeti.zpowCeil_self {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) : zpowCeil c c = c

The constant c is its own rounding.

theorem TauCeti.monotone_zpowCeil {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) : Monotone (zpowCeil c)

Rounding up is monotone.

@[simp]

theorem TauCeti.zpowCeil_zpowCeil {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (x : ℝ) : zpowCeil c (zpowCeil c x) = zpowCeil c x

Rounding up is idempotent.

theorem TauCeti.zpowCeil_eq_self_iff {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hx : 0 ≤ x) : zpowCeil c x = x ↔ x = 0 ∨ ∃ (n : ℤ), c ^ n = x

A nonnegative number is its own rounding exactly when it is 0 or an integer power of c.

theorem TauCeti.zpowCeil_le_iff {c x y : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hy : zpowCeil c y = y) : zpowCeil c x ≤ y ↔ x ≤ y

Rounding up is a closure operator onto c ^ ℤ ∪ {0}: for y in that set, zpowCeil c x ≤ y ↔ x ≤ y.

theorem TauCeti.zpowCeil_lt_zpow_iff {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (n : ℤ) : zpowCeil c x < c ^ n ↔ x ≤ c ^ (n + 1)

Discreteness of the rounded values: zpowCeil c x lies strictly below c ^ n exactly when x ≤ c ^ (n + 1). In particular zpowCeil c x < 1 ↔ x ≤ c.

theorem TauCeti.le_of_zpowCeil_eq_self_of_lt_one {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hx : zpowCeil c x = x) (h : x < 1) : x ≤ c

A number in c ^ ℤ ∪ {0} that is less than 1 = c ^ 0 is at most c.

theorem TauCeti.zpowCeil_zpow_mul {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (n : ℤ) (x : ℝ) : zpowCeil c (c ^ n * x) = c ^ n * zpowCeil c x

Rounding commutes with scaling by powers of c: zpowCeil c (c ^ n * x) = c ^ n * zpowCeil c x.

theorem TauCeti.zpowCeil_mul_le {c x : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (hx : 0 ≤ x) (y : ℝ) : zpowCeil c (x * y) ≤ zpowCeil c x * zpowCeil c y

Rounding up is submultiplicative on a nonnegative left factor: zpowCeil c (x * y) ≤ zpowCeil c x * zpowCeil c y.

theorem TauCeti.zpowCeil_norm_add_le_max {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [SeminormedAddGroup M] [IsUltrametricDist M] (m n : M) : zpowCeil c ‖m + n‖ ≤ max (zpowCeil c ‖m‖) (zpowCeil c ‖n‖)

Rounding preserves the ultrametric inequality.

theorem TauCeti.zpowCeil_norm_smul_le {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [SeminormedAddGroup M] {R : Type u_2} [SeminormedAddGroup R] [SMulZeroClass R M] [IsBoundedSMul R M] (a : R) (m : M) : zpowCeil c ‖a • m‖ ≤ zpowCeil c ‖a‖ * zpowCeil c ‖m‖

Rounding is compatible with contractive scalar actions: zpowCeil c ‖a • m‖ ≤ zpowCeil c ‖a‖ * zpowCeil c ‖m‖. When ‖a‖ lies in c ^ ℤ ∪ {0} (zpowCeil_eq_self_iff), the right-hand side is ‖a‖ * zpowCeil c ‖m‖.

noncomputable def TauCeti.zpowCeilAddGroupSeminorm {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (M : Type u_1) [SeminormedAddGroup M] [IsUltrametricDist M] : AddGroupSeminorm M

The norm of an ultrametric seminormed group rounded up to c ^ ℤ ∪ {0}, for 0 < c < 1. It satisfies ‖m‖ ≤ zpowCeil c ‖m‖ and, for ‖m‖ ≠ 0, c * zpowCeil c ‖m‖ < ‖m‖, so it is bounded-equivalent to the original norm.

@[simp]

theorem TauCeti.zpowCeilAddGroupSeminorm_apply {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (M : Type u_1) [SeminormedAddGroup M] [IsUltrametricDist M] (m : M) : (zpowCeilAddGroupSeminorm hc₀ hc₁ M) m = zpowCeil c ‖m‖

The rounded seminorm of m is the rounding of ‖m‖.

theorem TauCeti.isNonarchimedean_zpowCeilAddGroupSeminorm {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (M : Type u_1) [SeminormedAddGroup M] [IsUltrametricDist M] : IsNonarchimedean ⇑(zpowCeilAddGroupSeminorm hc₀ hc₁ M)

The rounded seminorm is ultrametric.

noncomputable def TauCeti.zpowCeilAddGroupNorm {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) (M : Type u_1) [NormedAddGroup M] [IsUltrametricDist M] : AddGroupNorm M

The norm of an ultrametric normed group rounded up to c ^ ℤ ∪ {0}, for 0 < c < 1, as a group norm.

@[simp]

theorem TauCeti.zpowCeilAddGroupNorm_apply {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [NormedAddGroup M] [IsUltrametricDist M] (m : M) : (zpowCeilAddGroupNorm hc₀ hc₁ M) m = zpowCeil c ‖m‖

The rounded norm of m is the rounding of ‖m‖.

@[reducible, inline]

noncomputable abbrev TauCeti.zpowCeilNormedAddCommGroup {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [NormedAddCommGroup M] [IsUltrametricDist M] : NormedAddCommGroup M

The rounded norm with the original uniformity and topology retained definitionally. In particular, completeness and continuity are unchanged.

theorem TauCeti.isUltrametricDist_zpowCeilNormedAddCommGroup {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [NormedAddCommGroup M] [IsUltrametricDist M] : IsUltrametricDist M

The compatible rounded norm is ultrametric.

theorem TauCeti.isBoundedSMul_zpowCeilNormedAddCommGroup {c : ℝ} (hc₀ : 0 < c) (hc₁ : c < 1) {M : Type u_1} [NormedAddCommGroup M] [IsUltrametricDist M] {R : Type u_2} [SeminormedRing R] [Module R M] [IsBoundedSMul R M] (hR : ∀ (a : R), zpowCeil c ‖a‖ = ‖a‖) : IsBoundedSMul R M

Rounding preserves a contractive scalar action when the scalar norms already lie in c ^ ℤ ∪ {0}. Without this hypothesis the original scalar norm need not act contractively.