Ultrametric norms

This file contains results on the behavior of norms in ultrametric groups.

Main results

• IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm: a normed additive group has an ultrametric iff the norm is nonarchimedean
• IsUltrametricDist.nonarchimedeanGroup and its additive version: instance showing that a commutative group with a nonarchimedean seminorm is a nonarchimedean topological group (i.e. there is a neighbourhood basis of the identity consisting of open subgroups).

Implementation details

Some results are proved first about nnnorm : X → ℝ≥0 because the bottom element in NNReal is 0, so easier to make statements about maxima of empty sets.

Tags

ultrametric, nonarchimedean

theorem IsUltrametricDist.norm_mul_le_max {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y : S) : ‖x * y‖ ≤ ‖x‖ ⊔ ‖y‖

theorem IsUltrametricDist.norm_add_le_max {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y : S) : ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_mul_le_max_norm {S' : Type u_2} [SeminormedGroup S'] (h : ∀ (x y : S'), ‖x * y‖ ≤ ‖x‖ ⊔ ‖y‖) : IsUltrametricDist S'

theorem IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm {S' : Type u_2} [SeminormedAddGroup S'] (h : ∀ (x y : S'), ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖) : IsUltrametricDist S'

theorem IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm {S' : Type u_4} [SeminormedAddGroup S'] (h : IsNonarchimedean norm) : IsUltrametricDist S'

theorem IsUltrametricDist.isNonarchimedean_norm {R : Type u_4} [SeminormedAddCommGroup R] [IsUltrametricDist R] : IsNonarchimedean fun (x : R) => ‖x‖

theorem IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_norm {R : Type u_4} [SeminormedAddCommGroup R] : IsUltrametricDist R ↔ IsNonarchimedean fun (x : R) => ‖x‖

theorem IsUltrametricDist.nnnorm_mul_le_max {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y : S) : ‖x * y‖₊ ≤ ‖x‖₊ ⊔ ‖y‖₊

theorem IsUltrametricDist.nnnorm_add_le_max {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y : S) : ‖x + y‖₊ ≤ ‖x‖₊ ⊔ ‖y‖₊

theorem IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm {S' : Type u_2} [SeminormedGroup S'] (h : ∀ (x y : S'), ‖x * y‖₊ ≤ ‖x‖₊ ⊔ ‖y‖₊) : IsUltrametricDist S'

theorem IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm {S' : Type u_2} [SeminormedAddGroup S'] (h : ∀ (x y : S'), ‖x + y‖₊ ≤ ‖x‖₊ ⊔ ‖y‖₊) : IsUltrametricDist S'

theorem IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_nnnorm {S' : Type u_4} [SeminormedAddGroup S'] (h : IsNonarchimedean (NNReal.toReal ∘ nnnorm)) : IsUltrametricDist S'

theorem IsUltrametricDist.isNonarchimedean_nnnorm {R : Type u_4} [SeminormedAddCommGroup R] [IsUltrametricDist R] : IsNonarchimedean fun (x : R) => ↑‖x‖₊

theorem IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm {R : Type u_4} [SeminormedAddCommGroup R] : IsUltrametricDist R ↔ IsNonarchimedean fun (x : R) => ↑‖x‖₊

theorem IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x‖ ≠ ‖y‖) : ‖x * y‖ = ‖x‖ ⊔ ‖y‖

All triangles are isosceles in an ultrametric normed group.

theorem IsUltrametricDist.norm_add_eq_max_of_norm_ne_norm {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x‖ ≠ ‖y‖) : ‖x + y‖ = ‖x‖ ⊔ ‖y‖

All triangles are isosceles in an ultrametric normed additive group.

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

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

theorem IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x‖₊ ≠ ‖y‖₊) : ‖x * y‖₊ = ‖x‖₊ ⊔ ‖y‖₊

All triangles are isosceles in an ultrametric normed group.

theorem IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x‖₊ ≠ ‖y‖₊) : ‖x + y‖₊ = ‖x‖₊ ⊔ ‖y‖₊

All triangles are isosceles in an ultrametric normed additive group.

theorem IsUltrametricDist.nnnorm_eq_of_mul_nnnorm_lt_max {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x * y‖₊ < ‖x‖₊ ⊔ ‖y‖₊) : ‖x‖₊ = ‖y‖₊

theorem IsUltrametricDist.nnnorm_eq_of_add_nnnorm_lt_max {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] {x y : S} (h : ‖x + y‖₊ < ‖x‖₊ ⊔ ‖y‖₊) : ‖x‖₊ = ‖y‖₊

theorem IsUltrametricDist.norm_div_eq_max_of_norm_div_ne_norm_div {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y z : S) (h : ‖x / y‖ ≠ ‖y / z‖) : ‖x / z‖ = ‖x / y‖ ⊔ ‖y / z‖

All triangles are isosceles in an ultrametric normed group.

theorem IsUltrametricDist.norm_sub_eq_max_of_norm_sub_ne_norm_sub {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y z : S) (h : ‖x - y‖ ≠ ‖y - z‖) : ‖x - z‖ = ‖x - y‖ ⊔ ‖y - z‖

All triangles are isosceles in an ultrametric normed additive group.

theorem IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x y z : S) (h : ‖x / y‖₊ ≠ ‖y / z‖₊) : ‖x / z‖₊ = ‖x / y‖₊ ⊔ ‖y / z‖₊

All triangles are isosceles in an ultrametric normed group.

theorem IsUltrametricDist.nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x y z : S) (h : ‖x - y‖₊ ≠ ‖y - z‖₊) : ‖x - z‖₊ = ‖x - y‖₊ ⊔ ‖y - z‖₊

All triangles are isosceles in an ultrametric normed additive group.

theorem IsUltrametricDist.nnnorm_pow_le {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x : S) (n : ℕ) : ‖x ^ n‖₊ ≤ ‖x‖₊

theorem IsUltrametricDist.nnnorm_nsmul_le {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (n : ℕ) : ‖n • x‖₊ ≤ ‖x‖₊

theorem IsUltrametricDist.norm_pow_le {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x : S) (n : ℕ) : ‖x ^ n‖ ≤ ‖x‖

theorem IsUltrametricDist.norm_nsmul_le {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (n : ℕ) : ‖n • x‖ ≤ ‖x‖

theorem IsUltrametricDist.nnnorm_zpow_le {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x : S) (z : ℤ) : ‖x ^ z‖₊ ≤ ‖x‖₊

theorem IsUltrametricDist.nnnorm_zsmul_le {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (z : ℤ) : ‖z • x‖₊ ≤ ‖x‖₊

theorem IsUltrametricDist.norm_zpow_le {S : Type u_1} [SeminormedGroup S] [IsUltrametricDist S] (x : S) (z : ℤ) : ‖x ^ z‖ ≤ ‖x‖

theorem IsUltrametricDist.norm_zsmul_le {S : Type u_1} [SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (z : ℤ) : ‖z • x‖ ≤ ‖x‖

def IsUltrametricDist.ball_openSubgroup (S : Type u_1) [SeminormedGroup S] [IsUltrametricDist S] {r : ℝ} (hr : 0 < r) : OpenSubgroup S

In a group with an ultrametric norm, open balls around 1 of positive radius are open subgroups.

Equations

• IsUltrametricDist.ball_openSubgroup S hr = { carrier := Metric.ball 1 r, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, isOpen' := ⋯ }

def IsUltrametricDist.ball_openAddSubgroup (S : Type u_1) [SeminormedAddGroup S] [IsUltrametricDist S] {r : ℝ} (hr : 0 < r) : OpenAddSubgroup S

In an additive group with an ultrametric norm, open balls around 0 of positive radius are open subgroups.

Equations

• IsUltrametricDist.ball_openAddSubgroup S hr = { carrier := Metric.ball 0 r, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, isOpen' := ⋯ }

def IsUltrametricDist.closedBall_openSubgroup (S : Type u_1) [SeminormedGroup S] [IsUltrametricDist S] {r : ℝ} (hr : 0 < r) : OpenSubgroup S

In a group with an ultrametric norm, closed balls around 1 of positive radius are open subgroups.

Equations

• IsUltrametricDist.closedBall_openSubgroup S hr = { carrier := Metric.closedBall 1 r, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, isOpen' := ⋯ }

def IsUltrametricDist.closedBall_openAddSubgroup (S : Type u_1) [SeminormedAddGroup S] [IsUltrametricDist S] {r : ℝ} (hr : 0 < r) : OpenAddSubgroup S

In an additive group with an ultrametric norm, closed balls around 0 of positive radius are open subgroups.

Equations

• IsUltrametricDist.closedBall_openAddSubgroup S hr = { carrier := Metric.closedBall 0 r, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, isOpen' := ⋯ }

instance IsUltrametricDist.nonarchimedeanGroup {M : Type u_1} [SeminormedCommGroup M] [IsUltrametricDist M] : NonarchimedeanGroup M

A commutative group with an ultrametric group seminorm is nonarchimedean (as a topological group, i.e. every neighborhood of 1 contains an open subgroup).

Equations

• ⋯ = ⋯

instance IsUltrametricDist.nonarchimedeanAddGroup {M : Type u_1} [SeminormedAddCommGroup M] [IsUltrametricDist M] : NonarchimedeanAddGroup M

A commutative additive group with an ultrametric group seminorm is nonarchimedean (as a topological group, i.e. every neighborhood of 0 contains an open subgroup).

Equations

• ⋯ = ⋯

theorem Finset.Nonempty.norm_prod_le_sup'_norm {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) : ‖∏ i ∈ s, f i‖ ≤ s.sup' hs fun (x : ι) => ‖f x‖

Nonarchimedean norm of a product is less than or equal the norm of any term in the product. This version is phrased using Finset.sup' and Finset.Nonempty due to Finset.sup operating over an OrderBot, which ℝ is not.

theorem Finset.Nonempty.norm_sum_le_sup'_norm {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) : ‖∑ i ∈ s, f i‖ ≤ s.sup' hs fun (x : ι) => ‖f x‖

Nonarchimedean norm of a sum is less than or equal the norm of any term in the sum. This version is phrased using Finset.sup' and Finset.Nonempty due to Finset.sup operating over an OrderBot, which ℝ is not.

theorem Finset.nnnorm_prod_le_sup_nnnorm {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ι → M) : ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun (x : ι) => ‖f x‖₊

Nonarchimedean norm of a product is less than or equal to the largest norm of a term in the product.

theorem Finset.nnnorm_sum_le_sup_nnnorm {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ι → M) : ‖∑ i ∈ s, f i‖₊ ≤ s.sup fun (x : ι) => ‖f x‖₊

Nonarchimedean norm of a sum is less than or equal to the largest norm of a term in the sum.

theorem IsUltrametricDist.nnnorm_prod_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M} {C : NNReal} (hC : ∀ i ∈ s, ‖f i‖₊ ≤ C) : ‖∏ i ∈ s, f i‖₊ ≤ C

Generalised ultrametric triangle inequality for finite products in commutative groups with an ultrametric norm.

theorem IsUltrametricDist.nnnorm_sum_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M} {C : NNReal} (hC : ∀ i ∈ s, ‖f i‖₊ ≤ C) : ‖∑ i ∈ s, f i‖₊ ≤ C

Generalised ultrametric triangle inequality for finite sums in additive commutative groups with an ultrametric norm.

theorem IsUltrametricDist.norm_prod_le_of_forall_le_of_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) {f : ι → M} {C : ℝ} (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∏ i ∈ s, f i‖ ≤ C

Generalised ultrametric triangle inequality for nonempty finite products in commutative groups with an ultrametric norm.

theorem IsUltrametricDist.norm_sum_le_of_forall_le_of_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) {f : ι → M} {C : ℝ} (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∑ i ∈ s, f i‖ ≤ C

Generalised ultrametric triangle inequality for nonempty finite sums in additive commutative groups with an ultrametric norm.

theorem IsUltrametricDist.norm_prod_le_of_forall_le_of_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M} {C : ℝ} (h_nonneg : 0 ≤ C) (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∏ i ∈ s, f i‖ ≤ C

Generalised ultrametric triangle inequality for finite products in commutative groups with an ultrametric norm.

theorem IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M} {C : ℝ} (h_nonneg : 0 ≤ C) (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∑ i ∈ s, f i‖ ≤ C

Generalised ultrametric triangle inequality for finite sums in additive commutative groups with an ultrametric norm.

theorem IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {t : Finset ι} (ht : t.Nonempty) (f : ι → M) : ∃ i ∈ t, ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Given a function f : ι → M and a nonempty finite set t ⊆ ι, we can always find i ∈ t such that ‖∏ j in t, f j‖ ≤ ‖f i‖.

theorem IsUltrametricDist.exists_norm_finset_sum_le_of_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {t : Finset ι} (ht : t.Nonempty) (f : ι → M) : ∃ i ∈ t, ‖∑ j ∈ t, f j‖ ≤ ‖f i‖

Given a function f : ι → M and a nonempty finite set t ⊆ ι, we can always find i ∈ t such that ‖∑ j in t, f j‖ ≤ ‖f i‖.

theorem IsUltrametricDist.exists_norm_finset_prod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι] (f : ι → M) : ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖

Given a function f : ι → M and a finite set t ⊆ ι, we can always find i : ι, belonging to t if t is nonempty, such that ‖∏ j in t, f j‖ ≤ ‖f i‖.

theorem IsUltrametricDist.exists_norm_finset_sum_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι] (f : ι → M) : ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ ‖∑ j ∈ t, f j‖ ≤ ‖f i‖

Given a function f : ι → M and a finite set t ⊆ ι, we can always find i : ι, belonging to t if t is nonempty, such that ‖∑ j in t, f j‖ ≤ ‖f i‖.

theorem IsUltrametricDist.exists_norm_multiset_prod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι] {f : ι → M} : ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Given a function f : ι → M and a multiset t : Multiset ι, we can always find i : ι, belonging to t if t is nonempty, such that ‖(s.map f).prod‖ ≤ ‖f i‖.

theorem IsUltrametricDist.exists_norm_multiset_sum_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι] {f : ι → M} : ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).sum‖ ≤ ‖f i‖

Given a function f : ι → M and a multiset t : Multiset ι, we can always find i : ι, belonging to t if t is nonempty, such that ‖(s.map f).sum‖ ≤ ‖f i‖.

theorem IsUltrametricDist.norm_tprod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (f : ι → M) : ‖∏' (i : ι), f i‖ ≤ ⨆ (i : ι), ‖f i‖

theorem IsUltrametricDist.norm_tsum_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (f : ι → M) : ‖∑' (i : ι), f i‖ ≤ ⨆ (i : ι), ‖f i‖

theorem IsUltrametricDist.nnnorm_tprod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (f : ι → M) : ‖∏' (i : ι), f i‖₊ ≤ ⨆ (i : ι), ‖f i‖₊

theorem IsUltrametricDist.nnnorm_tsum_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (f : ι → M) : ‖∑' (i : ι), f i‖₊ ≤ ⨆ (i : ι), ‖f i‖₊

theorem IsUltrametricDist.norm_tprod_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] [Nonempty ι] {f : ι → M} {C : ℝ} (h : ∀ (i : ι), ‖f i‖ ≤ C) : ‖∏' (i : ι), f i‖ ≤ C

theorem IsUltrametricDist.norm_tsum_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] [Nonempty ι] {f : ι → M} {C : ℝ} (h : ∀ (i : ι), ‖f i‖ ≤ C) : ‖∑' (i : ι), f i‖ ≤ C

theorem IsUltrametricDist.norm_tprod_le_of_forall_le_of_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (i : ι), ‖f i‖ ≤ C) : ‖∏' (i : ι), f i‖ ≤ C

theorem IsUltrametricDist.norm_tsum_le_of_forall_le_of_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (i : ι), ‖f i‖ ≤ C) : ‖∑' (i : ι), f i‖ ≤ C

theorem IsUltrametricDist.nnnorm_tprod_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : NNReal} (h : ∀ (i : ι), ‖f i‖₊ ≤ C) : ‖∏' (i : ι), f i‖₊ ≤ C

theorem IsUltrametricDist.nnnorm_tsum_le_of_forall_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : NNReal} (h : ∀ (i : ι), ‖f i‖₊ ≤ C) : ‖∑' (i : ι), f i‖₊ ≤ C