Documentation

Mathlib.Analysis.Normed.Group.Ultra

Ultrametric norms #

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

Main results #

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

All triangles are isosceles in an ultrametric normed additive group.

All triangles are isosceles in an ultrametric normed group.

All triangles are isosceles in an ultrametric normed additive group.

All triangles are isosceles in an ultrametric normed group.

All triangles are isosceles in an ultrametric normed additive group.

All triangles are isosceles in an ultrametric normed group.

All triangles are isosceles in an ultrametric normed additive group.

All triangles are isosceles in an ultrametric normed group.

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

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

          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
          • =

          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
          • =
          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) :
          is, 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.Nonempty.norm_prod_le_sup'_norm {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) (f : ιM) :
          is, 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.nnnorm_sum_le_sup_nnnorm {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ιM) :
          is, 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 Finset.nnnorm_prod_le_sup_nnnorm {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ιM) :
          is, 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 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 : is, f i‖₊ C) :
          is, f i‖₊ C

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

          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 : is, f i‖₊ C) :
          is, 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_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) {f : ιM} {C : } (hC : is, f i C) :
          is, 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_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty) {f : ιM} {C : } (hC : is, f i C) :
          is, 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_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ιM} {C : } (h_nonneg : 0 C) (hC : is, f i C) :
          is, 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_nonneg {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ιM} {C : } (h_nonneg : 0 C) (hC : is, f i C) :
          is, f i C

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

          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) :
          it, jt, 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_of_nonempty {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] {t : Finset ι} (ht : t.Nonempty) (f : ιM) :
          it, jt, 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 {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι] (f : ιM) :
          ∃ (i : ι), (t.Nonemptyi t) jt, 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_prod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι] (f : ιM) :
          ∃ (i : ι), (t.Nonemptyi t) jt, 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_sum_le {M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι] {f : ιM} :
          ∃ (i : ι), (s 0i 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.exists_norm_multiset_prod_le {M : Type u_1} {ι : Type u_2} [SeminormedCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι] {f : ιM} :
          ∃ (i : ι), (s 0i 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.norm_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 {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.nnnorm_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_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 {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_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.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.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
          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