Documentation

Mathlib.Analysis.Normed.Group.Constructions

Product of normed groups and other constructions #

This file constructs the infinity norm on finite products of normed groups and provides instances for type synonyms.

PUnit #

ULift #

instance ULift.norm {E : Type u_2} [Norm E] :
Equations
    @[simp]
    theorem ULift.norm_up {E : Type u_2} [Norm E] (x : E) :
    { down := x } = x
    @[simp]
    theorem ULift.norm_down {E : Type u_2} [Norm E] (x : ULift.{u_5, u_2} E) :
    instance ULift.nnnorm {E : Type u_2} [NNNorm E] :
    Equations
      @[simp]
      theorem ULift.nnnorm_up {E : Type u_2} [NNNorm E] (x : E) :
      { down := x }‖₊ = x‖₊
      @[simp]

      Additive, Multiplicative #

      instance Additive.toNorm {E : Type u_2} [Norm E] :
      Equations
        instance Multiplicative.toNorm {E : Type u_2} [Norm E] :
        Equations
          @[simp]
          theorem norm_toMul {E : Type u_2} [Norm E] (x : Additive E) :
          @[simp]
          theorem norm_ofMul {E : Type u_2} [Norm E] (x : E) :
          @[simp]
          @[simp]
          theorem norm_ofAdd {E : Type u_2} [Norm E] (x : E) :
          instance Additive.toNNNorm {E : Type u_2} [NNNorm E] :
          Equations
            Equations
              @[simp]
              @[simp]
              theorem nnnorm_ofMul {E : Type u_2} [NNNorm E] (x : E) :
              @[simp]

              Order dual #

              instance OrderDual.toNorm {E : Type u_2} [Norm E] :
              Equations
                @[simp]
                theorem norm_toDual {E : Type u_2} [Norm E] (x : E) :
                @[simp]
                theorem norm_ofDual {E : Type u_2} [Norm E] (x : Eᵒᵈ) :
                instance OrderDual.toNNNorm {E : Type u_2} [NNNorm E] :
                Equations
                  @[simp]
                  theorem nnnorm_toDual {E : Type u_2} [NNNorm E] (x : E) :
                  @[simp]
                  @[instance 100]
                  Equations
                    @[instance 100]
                    Equations
                      @[instance 100]
                      Equations
                        @[instance 100]
                        Equations
                          @[instance 100]
                          Equations
                            @[instance 100]
                            Equations

                              Binary product of normed groups #

                              instance Prod.toNorm {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] :
                              Norm (E × F)
                              Equations
                                theorem Prod.norm_def {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) :
                                @[simp]
                                theorem Prod.norm_mk {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E) (y : F) :
                                theorem norm_fst_le {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) :
                                theorem norm_snd_le {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (x : E × F) :
                                theorem norm_prod_le_iff {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] {x : E × F} {r : } :
                                instance Prod.seminormedGroup {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] :

                                Product of seminormed groups, using the sup norm.

                                Equations

                                  Product of seminormed groups, using the sup norm.

                                  Equations
                                    theorem Prod.nnnorm_def' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] (x : E × F) :

                                    Multiplicative version of Prod.nnnorm_def. Earlier, this names was used for the additive version.

                                    @[deprecated Prod.nnnorm_def' (since := "2025-01-02")]
                                    theorem Prod.nnorm_def {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] (x : E × F) :

                                    Alias of Prod.nnnorm_def'.


                                    Multiplicative version of Prod.nnnorm_def. Earlier, this names was used for the additive version.

                                    @[simp]
                                    theorem Prod.nnnorm_mk' {E : Type u_2} {F : Type u_3} [SeminormedGroup E] [SeminormedGroup F] (x : E) (y : F) :

                                    Multiplicative version of Prod.nnnorm_mk.

                                    @[simp]
                                    theorem Prod.nnnorm_mk {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E) (y : F) :

                                    Product of seminormed groups, using the sup norm.

                                    Equations

                                      Product of seminormed groups, using the sup norm.

                                      Equations
                                        instance Prod.normedGroup {E : Type u_2} {F : Type u_3} [NormedGroup E] [NormedGroup F] :

                                        Product of normed groups, using the sup norm.

                                        Equations
                                          instance Prod.normedAddGroup {E : Type u_2} {F : Type u_3} [NormedAddGroup E] [NormedAddGroup F] :

                                          Product of normed groups, using the sup norm.

                                          Equations
                                            instance Prod.normedCommGroup {E : Type u_2} {F : Type u_3} [NormedCommGroup E] [NormedCommGroup F] :

                                            Product of normed groups, using the sup norm.

                                            Equations

                                              Product of normed groups, using the sup norm.

                                              Equations

                                                Finite product of normed groups #

                                                instance Pi.seminormedGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] :
                                                SeminormedGroup ((i : ι) → G i)

                                                Finite product of seminormed groups, using the sup norm.

                                                Equations
                                                  instance Pi.seminormedAddGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] :
                                                  SeminormedAddGroup ((i : ι) → G i)

                                                  Finite product of seminormed groups, using the sup norm.

                                                  Equations
                                                    theorem Pi.norm_def' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) :
                                                    f = (Finset.univ.sup fun (b : ι) => f b‖₊)
                                                    theorem Pi.norm_def {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) :
                                                    f = (Finset.univ.sup fun (b : ι) => f b‖₊)
                                                    theorem Pi.nnnorm_def' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) :
                                                    f‖₊ = Finset.univ.sup fun (b : ι) => f b‖₊
                                                    theorem Pi.nnnorm_def {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) :
                                                    f‖₊ = Finset.univ.sup fun (b : ι) => f b‖₊
                                                    theorem pi_norm_le_iff_of_nonneg' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : } (hr : 0 r) :
                                                    x r ∀ (i : ι), x i r

                                                    The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

                                                    theorem pi_norm_le_iff_of_nonneg {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : } (hr : 0 r) :
                                                    x r ∀ (i : ι), x i r

                                                    The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

                                                    theorem pi_nnnorm_le_iff' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : NNReal} :
                                                    x‖₊ r ∀ (i : ι), x i‖₊ r
                                                    theorem pi_nnnorm_le_iff {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} :
                                                    x‖₊ r ∀ (i : ι), x i‖₊ r
                                                    theorem pi_norm_le_iff_of_nonempty' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) {r : } [Nonempty ι] :
                                                    f r ∀ (b : ι), f b r
                                                    theorem pi_norm_le_iff_of_nonempty {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) {r : } [Nonempty ι] :
                                                    f r ∀ (b : ι), f b r
                                                    theorem pi_norm_lt_iff' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : } (hr : 0 < r) :
                                                    x < r ∀ (i : ι), x i < r

                                                    The seminorm of an element in a product space is < r if and only if the norm of each component is.

                                                    theorem pi_norm_lt_iff {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : } (hr : 0 < r) :
                                                    x < r ∀ (i : ι), x i < r

                                                    The seminorm of an element in a product space is < r if and only if the norm of each component is.

                                                    theorem pi_nnnorm_lt_iff' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i} {r : NNReal} (hr : 0 < r) :
                                                    x‖₊ < r ∀ (i : ι), x i‖₊ < r
                                                    theorem pi_nnnorm_lt_iff {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i} {r : NNReal} (hr : 0 < r) :
                                                    x‖₊ < r ∀ (i : ι), x i‖₊ < r
                                                    theorem norm_le_pi_norm' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) (i : ι) :
                                                    theorem norm_le_pi_norm {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) (i : ι) :
                                                    theorem nnnorm_le_pi_nnnorm' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) (i : ι) :
                                                    theorem nnnorm_le_pi_nnnorm {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) (i : ι) :
                                                    theorem pi_norm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) :
                                                    fun (x : ι) => a a
                                                    theorem pi_norm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) :
                                                    fun (x : ι) => a a
                                                    theorem pi_nnnorm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) :
                                                    fun (x : ι) => a‖₊ a‖₊
                                                    theorem pi_nnnorm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) :
                                                    fun (x : ι) => a‖₊ a‖₊
                                                    @[simp]
                                                    theorem pi_norm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :
                                                    fun (_i : ι) => a = a
                                                    @[simp]
                                                    theorem pi_norm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :
                                                    fun (_i : ι) => a = a
                                                    @[simp]
                                                    theorem pi_nnnorm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :
                                                    fun (_i : ι) => a‖₊ = a‖₊
                                                    @[simp]
                                                    theorem pi_nnnorm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :
                                                    fun (_i : ι) => a‖₊ = a‖₊
                                                    theorem Pi.sum_norm_apply_le_norm' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) :
                                                    i : ι, f i Fintype.card ι f

                                                    The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                    theorem Pi.sum_norm_apply_le_norm {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) :
                                                    i : ι, f i Fintype.card ι f

                                                    The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                    theorem Pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i) :

                                                    The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                    theorem Pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i) :

                                                    The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

                                                    instance Pi.seminormedCommGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedCommGroup (G i)] :
                                                    SeminormedCommGroup ((i : ι) → G i)

                                                    Finite product of seminormed groups, using the sup norm.

                                                    Equations
                                                      instance Pi.seminormedAddCommGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (G i)] :
                                                      SeminormedAddCommGroup ((i : ι) → G i)

                                                      Finite product of seminormed groups, using the sup norm.

                                                      Equations
                                                        instance Pi.normedGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → NormedGroup (G i)] :
                                                        NormedGroup ((i : ι) → G i)

                                                        Finite product of normed groups, using the sup norm.

                                                        Equations
                                                          instance Pi.normedAddGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → NormedAddGroup (G i)] :
                                                          NormedAddGroup ((i : ι) → G i)

                                                          Finite product of seminormed groups, using the sup norm.

                                                          Equations
                                                            instance Pi.normedCommGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → NormedCommGroup (G i)] :
                                                            NormedCommGroup ((i : ι) → G i)

                                                            Finite product of normed groups, using the sup norm.

                                                            Equations
                                                              instance Pi.normedAddCommGroup {ι : Type u_1} {G : ιType u_4} [Fintype ι] [(i : ι) → NormedAddCommGroup (G i)] :
                                                              NormedAddCommGroup ((i : ι) → G i)

                                                              Finite product of seminormed groups, using the sup norm.

                                                              Equations
                                                                theorem Pi.nnnorm_single {ι : Type u_1} {G : ιType u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) :
                                                                theorem Pi.enorm_single {ι : Type u_1} {G : ιType u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) :
                                                                theorem Pi.norm_single {ι : Type u_1} {G : ιType u_4} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i) :

                                                                Multiplicative opposite #

                                                                The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

                                                                Note that we do not provide this more generally as Norm Eᵐᵒᵖ, as this is not always a good choice of norm in the multiplicative SeminormedGroup E case.

                                                                We could repeat this instance to provide a [SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ instance, but that case would likely never be used.

                                                                Equations