Mathlib.Analysis.Normed.Group.Constructions

PUnit.normedAddCommGroup instance

: NormedAddCommGroup PUnit

Full source

instance normedAddCommGroup : NormedAddCommGroup PUnit where
  norm := Function.const _ 0
  dist_eq _ _ := rfl

Normed Additive Commutative Group Structure on the Unit Type

Informal description

The trivial additive commutative group `PUnit` (the type with a single element) is equipped with a normed group structure where the norm of its unique element is zero.

PUnit.norm_eq_zero theorem

(x : PUnit) : ‖x‖ = 0

Full source

@[simp] lemma norm_eq_zero (x : PUnit) : ‖x‖ = 0 := rfl

Norm Vanishes on Unit Type

Informal description

For any element $x$ of the unit type `PUnit`, the norm of $x$ is zero, i.e., $\|x\| = 0$.

ULift.norm instance

: Norm (ULift E)

Full source

instance norm : Norm (ULift E) where norm x := ‖x.down‖

Norm Structure on Lifted Types

Informal description

For any normed type $E$, the type `ULift E` (which represents a lifted version of $E$) inherits a norm structure where the norm of an element $x$ in `ULift E` is equal to the norm of its underlying element in $E$.

ULift.norm_def theorem

(x : ULift E) : ‖x‖ = ‖x.down‖

Full source

lemma norm_def (x : ULift E) : ‖x‖ = ‖x.down‖ := rfl

Norm Preservation in Lifted Types

Informal description

For any element $x$ in the lifted type $\mathrm{ULift}\, E$, the norm of $x$ is equal to the norm of its underlying element $x.\mathrm{down}$ in $E$, i.e., $\|x\| = \|x.\mathrm{down}\|$.

ULift.norm_up theorem

(x : E) : ‖ULift.up x‖ = ‖x‖

Full source

@[simp] lemma norm_up (x : E) : ‖ULift.up x‖ = ‖x‖ := rfl

Norm Preservation under Lifting: $\|\text{up}\,x\| = \|x\|$

Informal description

For any element $x$ in a normed group $E$, the norm of the lifted element $\text{ULift.up}\,x$ is equal to the norm of $x$, i.e., $\|\text{ULift.up}\,x\| = \|x\|$.

ULift.norm_down theorem

(x : ULift E) : ‖x.down‖ = ‖x‖

Full source

@[simp] lemma norm_down (x : ULift E) : ‖x.down‖ = ‖x‖ := rfl

Norm preservation under universe-lifting down projection

Informal description

For any element $x$ in the universe-lifted normed group $\operatorname{ULift} E$, the norm of the underlying element $x.\mathrm{down}$ in $E$ is equal to the norm of $x$ in $\operatorname{ULift} E$, i.e., $\|x.\mathrm{down}\| = \|x\|$.

ULift.nnnorm instance

: NNNorm (ULift E)

Full source

instance nnnorm : NNNorm (ULift E) where nnnorm x := ‖x.down‖₊

Non-Negative Norm Structure on Universe-Lifted Normed Groups

Informal description

For any normed group $E$, the type `ULift E` (a universe-lifted version of $E$) is equipped with a non-negative norm structure, where the norm of a lifted element is equal to the norm of its underlying element.

ULift.nnnorm_def theorem

(x : ULift E) : ‖x‖₊ = ‖x.down‖₊

Full source

lemma nnnorm_def (x : ULift E) : ‖x‖₊ = ‖x.down‖₊ := rfl

Non-Negative Norm Equality for Universe-Lifted Elements

Informal description

For any element $x$ in the universe-lifted normed group $\operatorname{ULift} E$, the non-negative norm of $x$ is equal to the non-negative norm of its underlying element $x.\operatorname{down}$ in $E$, i.e., $\|x\|_{\mathbb{R}_{\geq 0}} = \|x.\operatorname{down}\|_{\mathbb{R}_{\geq 0}}$.

ULift.nnnorm_up theorem

(x : E) : ‖ULift.up x‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_up (x : E) : ‖ULift.up x‖₊ = ‖x‖₊ := rfl

Preservation of Non-Negative Norm under Universe Lifting

Informal description

For any element $x$ in a normed group $E$, the non-negative norm of the universe-lifted element $\operatorname{ULift.up}(x)$ is equal to the non-negative norm of $x$, i.e., $\|\operatorname{ULift.up}(x)\|_{\mathbb{R}_{\geq 0}} = \|x\|_{\mathbb{R}_{\geq 0}}$.

ULift.nnnorm_down theorem

(x : ULift E) : ‖x.down‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_down (x : ULift E) : ‖x.down‖₊ = ‖x‖₊ := rfl

Equality of Norms for Underlying Element in Universe-Lifted Normed Group

Informal description

For any element $x$ in the universe-lifted normed group $\operatorname{ULift} E$, the non-negative norm of its underlying element $x.\mathrm{down}$ is equal to the non-negative norm of $x$ itself, i.e., $\|x.\mathrm{down}\|₊ = \|x\|₊$.

ULift.seminormedGroup instance

[SeminormedGroup E] : SeminormedGroup (ULift E)

Full source

@[to_additive]
instance seminormedGroup [SeminormedGroup E] : SeminormedGroup (ULift E) :=
  SeminormedGroup.induced _ _
  { toFun := ULift.down,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl : ULiftULift E →* E }

Seminormed Group Structure on Universe-Lifted Types

Informal description

For any seminormed group $E$, the universe-lifted type $\mathrm{ULift}\,E$ is also a seminormed group, with the norm and group operations inherited from $E$.

ULift.seminormedCommGroup instance

[SeminormedCommGroup E] : SeminormedCommGroup (ULift E)

Full source

@[to_additive]
instance seminormedCommGroup [SeminormedCommGroup E] : SeminormedCommGroup (ULift E) :=
  SeminormedCommGroup.induced _ _
  { toFun := ULift.down,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl : ULiftULift E →* E }

Seminormed Commutative Group Structure on Universe-Lifted Types

Informal description

For any seminormed commutative group $E$, the universe-lifted type $\mathrm{ULift}\,E$ is also a seminormed commutative group, with the norm and group operations inherited from $E$.

ULift.normedGroup instance

[NormedGroup E] : NormedGroup (ULift E)

Full source

@[to_additive]
instance normedGroup [NormedGroup E] : NormedGroup (ULift E) :=
  NormedGroup.induced _ _
  { toFun := ULift.down,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl : ULiftULift E →* E }
  down_injective

Normed Group Structure on Universe-Lifted Types

Informal description

For any normed group $E$, the universe-lifted type $\mathrm{ULift}\,E$ is also a normed group, with the norm and group operations inherited from $E$.

ULift.normedCommGroup instance

[NormedCommGroup E] : NormedCommGroup (ULift E)

Full source

@[to_additive]
instance normedCommGroup [NormedCommGroup E] : NormedCommGroup (ULift E) :=
  NormedCommGroup.induced _ _
  { toFun := ULift.down,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl : ULiftULift E →* E }
  down_injective

Normed Commutative Group Structure on Universe-Lifted Types

Informal description

For any normed commutative group $E$, the universe-lifted type $\mathrm{ULift}\,E$ is also a normed commutative group, with the norm and group operations inherited from $E$.

Additive.toNorm instance

: Norm (Additive E)

Full source

instance Additive.toNorm : Norm (Additive E) := ‹Norm E›

Norm on Additive Group

Informal description

The additive version of a normed group $E$ inherits a norm structure, where the norm of an element in $\text{Additive } E$ is defined to be equal to the norm of the corresponding element in $E$.

Multiplicative.toNorm instance

: Norm (Multiplicative E)

Full source

instance Multiplicative.toNorm : Norm (Multiplicative E) := ‹Norm E›

Norm on Multiplicative Version of a Normed Group

Informal description

The multiplicative version of a normed group $E$ inherits a norm structure, where the norm of an element in $\text{Multiplicative } E$ is equal to the norm of its corresponding element in $E$.

norm_toMul theorem

(x : Additive E) : ‖(x.toMul : E)‖ = ‖x‖

Full source

@[simp] lemma norm_toMul (x : Additive E) : ‖(x.toMul : E)‖ = ‖x‖ := rfl

Norm Preservation under Additive-to-Multiplicative Conversion

Informal description

For any element $x$ in the additive version of a normed group $E$, the norm of its corresponding element in $E$ (obtained via the `toMul` operation) is equal to the norm of $x$, i.e., $\|x_{\text{mul}}\| = \|x\|$.

norm_ofMul theorem

(x : E) : ‖ofMul x‖ = ‖x‖

Full source

@[simp] lemma norm_ofMul (x : E) : ‖ofMul x‖ = ‖x‖ := rfl

Norm Preservation in Additive Version of a Normed Group

Informal description

For any element $x$ in a normed group $E$, the norm of $\text{ofMul}\,x$ in the additive version of $E$ is equal to the norm of $x$ in $E$, i.e., $\|\text{ofMul}\,x\| = \|x\|$.

norm_toAdd theorem

(x : Multiplicative E) : ‖(x.toAdd : E)‖ = ‖x‖

Full source

@[simp] lemma norm_toAdd (x : Multiplicative E) : ‖(x.toAdd : E)‖ = ‖x‖ := rfl

Norm Preservation under Multiplicative-to-Additive Conversion

Informal description

For any element $x$ in the multiplicative version of a normed group $E$, the norm of its corresponding element in $E$ (obtained via the `toAdd` operation) is equal to the norm of $x$, i.e., $\|x_{\text{add}}\| = \|x\|$.

norm_ofAdd theorem

(x : E) : ‖ofAdd x‖ = ‖x‖

Full source

@[simp] lemma norm_ofAdd (x : E) : ‖ofAdd x‖ = ‖x‖ := rfl

Norm Preservation under Additive-to-Multiplicative Conversion

Informal description

For any element $x$ in a normed group $E$, the norm of $\text{ofAdd}\,x$ in the multiplicative version of $E$ is equal to the norm of $x$ in $E$, i.e., $\|\text{ofAdd}\,x\| = \|x\|$.

Additive.toNNNorm instance

: NNNorm (Additive E)

Full source

instance Additive.toNNNorm : NNNorm (Additive E) := ‹NNNorm E›

Non-Negative Norm on Additive Group

Informal description

The additive version of a normed group $E$ inherits a non-negative norm structure, where the norm of an element in the additive group is equal to the norm of its corresponding element in the original multiplicative group.

Multiplicative.toNNNorm instance

: NNNorm (Multiplicative E)

Full source

instance Multiplicative.toNNNorm : NNNorm (Multiplicative E) := ‹NNNorm E›

Non-negative Norm on Multiplicative Normed Group

Informal description

The multiplicative version of a normed group $E$ inherits a non-negative norm structure, where the norm of an element $x$ in the multiplicative group is equal to the norm of $x$ in the original additive group.

nnnorm_toMul theorem

(x : Additive E) : ‖(x.toMul : E)‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_toMul (x : Additive E) : ‖(x.toMul : E)‖₊ = ‖x‖₊ := rfl

Preservation of Non-Negative Norm under Multiplicative Conversion in Additive Group

Informal description

For any element $x$ in the additive version of a normed group $E$, the non-negative norm of its multiplicative counterpart (denoted by $x.\text{toMul}$) is equal to the non-negative norm of $x$, i.e., $\|x.\text{toMul}\|_+ = \|x\|_+$.

nnnorm_ofMul theorem

(x : E) : ‖ofMul x‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_ofMul (x : E) : ‖ofMul x‖₊ = ‖x‖₊ := rfl

Preservation of Non-Negative Norm under Multiplicative Conversion

Informal description

For any element $x$ in a normed group $E$, the non-negative norm of the multiplicative version of $x$ (denoted by $\text{ofMul } x$) is equal to the non-negative norm of $x$ in the original group, i.e., $\|\text{ofMul } x\|_+ = \|x\|_+$.

nnnorm_toAdd theorem

(x : Multiplicative E) : ‖(x.toAdd : E)‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_toAdd (x : Multiplicative E) : ‖(x.toAdd : E)‖₊ = ‖x‖₊ := rfl

Preservation of Non-Negative Norm under Additive Conversion in Multiplicative Group

Informal description

For any element $x$ in the multiplicative version of a normed group $E$, the non-negative norm of its additive counterpart (denoted by $x.\text{toAdd}$) is equal to the non-negative norm of $x$, i.e., $\|x.\text{toAdd}\|_+ = \|x\|_+$.

nnnorm_ofAdd theorem

(x : E) : ‖ofAdd x‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_ofAdd (x : E) : ‖ofAdd x‖₊ = ‖x‖₊ := rfl

Preservation of Non-Negative Norm under Additive Conversion

Informal description

For any element $x$ in a normed group $E$, the non-negative norm of $x$ in its additive version (denoted by $\text{ofAdd } x$) is equal to the non-negative norm of $x$ in the original group, i.e., $\|\text{ofAdd } x\|_+ = \|x\|_+$.

Additive.seminormedAddGroup instance

[SeminormedGroup E] : SeminormedAddGroup (Additive E)

Full source

instance Additive.seminormedAddGroup [SeminormedGroup E] : SeminormedAddGroup (Additive E) where
  dist_eq x y := dist_eq_norm_div x.toMul y.toMul

Seminormed Additive Group Structure on Additive of a Seminormed Group

Informal description

For any seminormed group $E$, the additive version $\text{Additive } E$ is a seminormed additive group with the same norm structure.

Multiplicative.seminormedGroup instance

[SeminormedAddGroup E] : SeminormedGroup (Multiplicative E)

Full source

instance Multiplicative.seminormedGroup [SeminormedAddGroup E] :
    SeminormedGroup (Multiplicative E) where
  dist_eq x y := dist_eq_norm_sub x.toAdd y.toAdd

Seminormed Group Structure on Multiplicative Version of a Seminormed Additive Group

Informal description

For any seminormed additive group $E$, the multiplicative version $\text{Multiplicative } E$ is a seminormed group with the same norm structure.

Additive.seminormedCommGroup instance

[SeminormedCommGroup E] : SeminormedAddCommGroup (Additive E)

Full source

instance Additive.seminormedCommGroup [SeminormedCommGroup E] :
    SeminormedAddCommGroup (Additive E) :=
  { Additive.seminormedAddGroup with
    add_comm := add_comm }

Seminormed Additive Commutative Group Structure on Additive of a Seminormed Commutative Group

Informal description

For any seminormed commutative group $E$, the additive version $\text{Additive } E$ is a seminormed additive commutative group with the same norm structure.

Multiplicative.seminormedAddCommGroup instance

[SeminormedAddCommGroup E] : SeminormedCommGroup (Multiplicative E)

Full source

instance Multiplicative.seminormedAddCommGroup [SeminormedAddCommGroup E] :
    SeminormedCommGroup (Multiplicative E) :=
  { Multiplicative.seminormedGroup with
    mul_comm := mul_comm }

Seminormed Commutative Group Structure on Multiplicative Version of a Seminormed Additive Commutative Group

Informal description

For any seminormed additive commutative group $E$, the multiplicative version $\text{Multiplicative } E$ is a seminormed commutative group with the same norm structure.

Additive.normedAddGroup instance

[NormedGroup E] : NormedAddGroup (Additive E)

Full source

instance Additive.normedAddGroup [NormedGroup E] : NormedAddGroup (Additive E) :=
  { Additive.seminormedAddGroup with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Additive Group Structure on Additive of a Normed Group

Informal description

For any normed group $E$, the additive version $\text{Additive } E$ is a normed additive group with the same norm structure.

Multiplicative.normedGroup instance

[NormedAddGroup E] : NormedGroup (Multiplicative E)

Full source

instance Multiplicative.normedGroup [NormedAddGroup E] : NormedGroup (Multiplicative E) :=
  { Multiplicative.seminormedGroup with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Group Structure on Multiplicative Version of a Normed Additive Group

Informal description

For any normed additive group $E$, the multiplicative version $\text{Multiplicative } E$ is a normed group with the same norm structure.

Additive.normedAddCommGroup instance

[NormedCommGroup E] : NormedAddCommGroup (Additive E)

Full source

instance Additive.normedAddCommGroup [NormedCommGroup E] : NormedAddCommGroup (Additive E) :=
  { Additive.seminormedAddGroup with
    add_comm := add_comm
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Additive Commutative Group Structure on Additive of a Normed Commutative Group

Informal description

For any normed commutative group $E$, the additive version $\text{Additive } E$ is a normed additive commutative group with the same norm structure.

Multiplicative.normedCommGroup instance

[NormedAddCommGroup E] : NormedCommGroup (Multiplicative E)

Full source

instance Multiplicative.normedCommGroup [NormedAddCommGroup E] :
    NormedCommGroup (Multiplicative E) :=
  { Multiplicative.seminormedGroup with
    mul_comm := mul_comm
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Commutative Group Structure on Multiplicative Version of a Normed Additive Commutative Group

Informal description

For any normed additive commutative group $E$, the multiplicative version $\text{Multiplicative } E$ is a normed commutative group with the same norm structure.

OrderDual.toNorm instance

: Norm Eᵒᵈ

Full source

instance OrderDual.toNorm : Norm Eᵒᵈ := ‹Norm E›

Norm on Order Dual of a Normed Group

Informal description

The order dual $E^\text{op}$ of a normed group $E$ inherits a norm structure, where the norm of an element in $E^\text{op}$ is equal to its norm in $E$.

norm_toDual theorem

(x : E) : ‖toDual x‖ = ‖x‖

Full source

@[simp] lemma norm_toDual (x : E) : ‖toDual x‖ = ‖x‖ := rfl

Norm Preservation under Order Dual Map: $\|\text{toDual}(x)\| = \|x\|$

Informal description

For any element $x$ in a normed group $E$, the norm of its image under the order dual map $\text{toDual}$ is equal to the norm of $x$, i.e., $\|\text{toDual}(x)\| = \|x\|$.

norm_ofDual theorem

(x : Eᵒᵈ) : ‖ofDual x‖ = ‖x‖

Full source

@[simp] lemma norm_ofDual (x : Eᵒᵈ) : ‖ofDual x‖ = ‖x‖ := rfl

Norm Preservation under Order Dual Reversal

Informal description

For any element $x$ in the order dual $E^{\text{op}}$ of a normed group $E$, the norm of its image under the order dual reversal map $\text{ofDual}$ is equal to the norm of $x$, i.e., $\|\text{ofDual}(x)\| = \|x\|$.

OrderDual.toNNNorm instance

: NNNorm Eᵒᵈ

Full source

instance OrderDual.toNNNorm : NNNorm Eᵒᵈ := ‹NNNorm E›

Non-Negative Norm on Order Dual

Informal description

The order dual $E^{\text{op}}$ of a normed group $E$ inherits a non-negative norm structure.

nnnorm_toDual theorem

(x : E) : ‖toDual x‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_toDual (x : E) : ‖toDual x‖₊ = ‖x‖₊ := rfl

Non-Negative Norm Preservation under Order Dualization

Informal description

For any element $x$ in a normed group $E$, the non-negative norm of the order dual of $x$ is equal to the non-negative norm of $x$, i.e., $\| \text{toDual}(x) \|_+ = \|x\|_+$.

nnnorm_ofDual theorem

(x : Eᵒᵈ) : ‖ofDual x‖₊ = ‖x‖₊

Full source

@[simp] lemma nnnorm_ofDual (x : Eᵒᵈ) : ‖ofDual x‖₊ = ‖x‖₊ := rfl

Non-Negative Norm Preservation under Order Dual Reversal

Informal description

For any element $x$ in the order dual $E^{\text{op}}$ of a normed group $E$, the non-negative norm of the element obtained by applying the `ofDual` function to $x$ is equal to the non-negative norm of $x$, i.e., $\|\text{ofDual}(x)\|_+ = \|x\|_+$.

OrderDual.seminormedGroup instance

[SeminormedGroup E] : SeminormedGroup Eᵒᵈ

Full source

@[to_additive]
instance (priority := 100) seminormedGroup [SeminormedGroup E] : SeminormedGroup Eᵒᵈ :=
  ‹SeminormedGroup E›

Order Dual of a Seminormed Group is a Seminormed Group

Informal description

For any seminormed group $E$, the order dual $E^{\text{op}}$ is also a seminormed group with the same norm structure.

OrderDual.seminormedCommGroup instance

[SeminormedCommGroup E] : SeminormedCommGroup Eᵒᵈ

Full source

@[to_additive]
instance (priority := 100) seminormedCommGroup [SeminormedCommGroup E] : SeminormedCommGroup Eᵒᵈ :=
  ‹SeminormedCommGroup E›

Order Dual of a Commutative Seminormed Group is a Commutative Seminormed Group

Informal description

For any commutative seminormed group $E$, the order dual $E^{\text{op}}$ is also a commutative seminormed group with the same norm structure.

OrderDual.normedGroup instance

[NormedGroup E] : NormedGroup Eᵒᵈ

Full source

@[to_additive]
instance (priority := 100) normedGroup [NormedGroup E] : NormedGroup Eᵒᵈ := ‹NormedGroup E›

Order Dual of a Normed Group is a Normed Group

Informal description

For any normed group $E$, the order dual $E^{\text{op}}$ is also a normed group with the same norm structure.

OrderDual.normedCommGroup instance

[NormedCommGroup E] : NormedCommGroup Eᵒᵈ

Full source

@[to_additive]
instance (priority := 100) normedCommGroup [NormedCommGroup E] : NormedCommGroup Eᵒᵈ :=
  ‹NormedCommGroup E›

Order Dual of a Commutative Normed Group is a Commutative Normed Group

Informal description

For any commutative normed group $E$, the order dual $E^{\text{op}}$ is also a commutative normed group with the same norm structure.

Prod.toNorm instance

: Norm (E × F)

Full source

instance Prod.toNorm : Norm (E × F) where norm x := ‖x.1‖‖x.1‖ ⊔ ‖x.2‖

Norm on the Product of Normed Groups

Informal description

For any two normed groups $E$ and $F$, the product $E \times F$ is equipped with a norm defined by $\|(x, y)\| = \max(\|x\|, \|y\|)$ for any $(x, y) \in E \times F$.

Prod.norm_def theorem

(x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖

Full source

lemma Prod.norm_def (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖ := rfl

Norm of a Pair Equals Maximum of Component Norms

Informal description

For any element $(x, y)$ in the product $E \times F$ of two normed groups, the norm of $(x, y)$ is equal to the maximum of the norms of $x$ and $y$, i.e., $\|(x, y)\| = \max(\|x\|, \|y\|)$.

Prod.norm_mk theorem

(x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖

Full source

@[simp] lemma Prod.norm_mk (x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖ := rfl

Norm of Pair Equals Maximum of Component Norms

Informal description

For any elements $x$ in a normed group $E$ and $y$ in a normed group $F$, the norm of the pair $(x, y)$ in the product space $E \times F$ is equal to the maximum of the norms of $x$ and $y$, i.e., $\|(x, y)\| = \max(\|x\|, \|y\|)$.

norm_fst_le theorem

(x : E × F) : ‖x.1‖ ≤ ‖x‖

Full source

lemma norm_fst_le (x : E × F) : ‖x.1‖ ≤ ‖x‖ := le_max_left _ _

Norm of First Component Bounded by Product Norm

Informal description

For any element $x = (x_1, x_2)$ in the product $E \times F$ of normed groups, the norm of the first component $x_1$ is bounded by the norm of $x$, i.e., $\|x_1\| \leq \|x\|$.

norm_snd_le theorem

(x : E × F) : ‖x.2‖ ≤ ‖x‖

Full source

lemma norm_snd_le (x : E × F) : ‖x.2‖ ≤ ‖x‖ := le_max_right _ _

Norm of Second Component Bounded by Product Norm

Informal description

For any element $x = (x_1, x_2)$ in the product $E \times F$ of normed groups, the norm of the second component is bounded by the norm of $x$, i.e., $\|x_2\| \leq \|x\|$.

norm_prod_le_iff theorem

: ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r

Full source

lemma norm_prod_le_iff : ‖x‖‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r := max_le_iff

Norm Bound Characterization for Product of Normed Groups: $\|x\| \leq r \leftrightarrow \|x_1\| \leq r \land \|x_2\| \leq r$

Informal description

For any element $x = (x_1, x_2)$ in the product $E \times F$ of normed groups and any real number $r$, the norm of $x$ satisfies $\|x\| \leq r$ if and only if both $\|x_1\| \leq r$ and $\|x_2\| \leq r$ hold.

Prod.seminormedGroup instance

: SeminormedGroup (E × F)

Full source

/-- Product of seminormed groups, using the sup norm. -/
@[to_additive "Product of seminormed groups, using the sup norm."]
instance Prod.seminormedGroup : SeminormedGroup (E × F) where
  dist_eq x y := by
    simp only [Prod.norm_def, Prod.dist_eq, dist_eq_norm_div, Prod.fst_div, Prod.snd_div]

Product of Seminormed Groups with Sup Norm

Informal description

For any seminormed groups $E$ and $F$, the product $E \times F$ is also a seminormed group with the norm defined by $\|(x, y)\| = \max(\|x\|, \|y\|)$ for any $(x, y) \in E \times F$.

Prod.nnnorm_def' theorem

(x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

Full source

/-- Multiplicative version of `Prod.nnnorm_def`.
Earlier, this names was used for the additive version. -/
@[to_additive Prod.nnnorm_def]
lemma Prod.nnnorm_def' (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ := rfl

Seminorm of Product Element Equals Maximum of Component Seminorms

Informal description

For any element $x = (x_1, x_2)$ in the product $E \times F$ of seminormed groups, the seminorm of $x$ is given by $\|x\| = \max(\|x_1\|, \|x_2\|)$, where $\|\cdot\|$ denotes the seminorm on the respective groups.

Prod.nnnorm_mk' theorem

(x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊

Full source

/-- Multiplicative version of `Prod.nnnorm_mk`. -/
@[to_additive (attr := simp) Prod.nnnorm_mk]
lemma Prod.nnnorm_mk' (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊ := rfl

Seminorm of Product Elements is Maximum of Seminorms

Informal description

For any elements $x$ in a seminormed group $E$ and $y$ in a seminormed group $F$, the seminorm of the pair $(x, y)$ in the product group $E \times F$ is given by the maximum of the seminorms of $x$ and $y$, i.e., $\|(x, y)\|_+ = \max(\|x\|_+, \|y\|_+)$.

Prod.seminormedCommGroup instance

[SeminormedCommGroup E] [SeminormedCommGroup F] : SeminormedCommGroup (E × F)

Full source

/-- Product of seminormed groups, using the sup norm. -/
@[to_additive "Product of seminormed groups, using the sup norm."]
instance seminormedCommGroup [SeminormedCommGroup E] [SeminormedCommGroup F] :
    SeminormedCommGroup (E × F) :=
  { Prod.seminormedGroup with
    mul_comm := mul_comm }

Product of Seminormed Commutative Groups with Sup Norm

Informal description

For any seminormed commutative groups $E$ and $F$, the product $E \times F$ is also a seminormed commutative group with the norm defined by $\|(x, y)\| = \max(\|x\|, \|y\|)$ for any $(x, y) \in E \times F$.

Prod.normedGroup instance

[NormedGroup E] [NormedGroup F] : NormedGroup (E × F)

Full source

/-- Product of normed groups, using the sup norm. -/
@[to_additive "Product of normed groups, using the sup norm."]
instance normedGroup [NormedGroup E] [NormedGroup F] : NormedGroup (E × F) :=
  { Prod.seminormedGroup with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Group Structure on Product Types with Supremum Norm

Informal description

For any normed groups $E$ and $F$, the product $E \times F$ is also a normed group with the norm defined by $\|(x, y)\| = \max(\|x\|, \|y\|)$ for any $(x, y) \in E \times F$.

Prod.normedCommGroup instance

[NormedCommGroup E] [NormedCommGroup F] : NormedCommGroup (E × F)

Full source

/-- Product of normed groups, using the sup norm. -/
@[to_additive "Product of normed groups, using the sup norm."]
instance normedCommGroup [NormedCommGroup E] [NormedCommGroup F] : NormedCommGroup (E × F) :=
  { Prod.seminormedGroup with
    mul_comm := mul_comm
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Commutative Group Structure on Binary Products with Sup Norm

Informal description

For any normed commutative groups $E$ and $F$, the product $E \times F$ is also a normed commutative group with the norm defined by $\|(x, y)\| = \max(\|x\|, \|y\|)$ for any $(x, y) \in E \times F$.

Pi.seminormedGroup instance

: SeminormedGroup (∀ i, G i)

Full source

/-- Finite product of seminormed groups, using the sup norm. -/
@[to_additive "Finite product of seminormed groups, using the sup norm."]
instance Pi.seminormedGroup : SeminormedGroup (∀ i, G i) where
  norm f := ↑(Finset.univ.sup fun b => ‖f b‖₊)
  dist_eq x y :=
    congr_arg (toReal : ℝ≥0 → ℝ) <|
      congr_arg (Finset.sup Finset.univ) <|
        funext fun a => show nndist (x a) (y a) = ‖x a / y a‖₊ from nndist_eq_nnnorm_div (x a) (y a)

Seminormed Group Structure on Product Types with Supremum Norm

Informal description

For any family of seminormed groups $(G_i)_{i \in I}$, the product type $\prod_{i \in I} G_i$ is also a seminormed group with the supremum norm $\|f\| = \sup_{i \in I} \|f(i)\|$.

Pi.norm_def' theorem

: ‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊)

Full source

@[to_additive Pi.norm_def]
lemma Pi.norm_def' : ‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊) := rfl

Norm of Finite Product as Supremum of Component Norms

Informal description

Pi.nnnorm_def' theorem

: ‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊

Full source

@[to_additive Pi.nnnorm_def]
lemma Pi.nnnorm_def' : ‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊ := Subtype.eta _ _

Supremum Norm Characterization for Finite Product of Normed Groups

Informal description

For a function $f$ in a finite product of normed groups, the supremum norm $\|f\|$ is equal to the supremum of the norms $\|f(b)\|$ over all indices $b$ in the finite indexing set, i.e., $\|f\| = \sup_{b} \|f(b)\|$.

pi_norm_le_iff_of_nonneg' theorem

(hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ i, ‖x i‖ ≤ r

Full source

/-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
component is. -/
@[to_additive pi_norm_le_iff_of_nonneg "The seminorm of an element in a product space is `≤ r` if
and only if the norm of each component is."]
lemma pi_norm_le_iff_of_nonneg' (hr : 0 ≤ r) : ‖x‖‖x‖ ≤ r ↔ ∀ i, ‖x i‖ ≤ r := by
  simp only [← dist_one_right, dist_pi_le_iff hr, Pi.one_apply]

Norm Bound in Product Space via Componentwise Bounds

Informal description

For any real number $r \geq 0$ and any element $x$ in a product of normed groups, the norm of $x$ satisfies $\|x\| \leq r$ if and only if for every index $i$, the norm of the $i$-th component $\|x_i\| \leq r$.

pi_nnnorm_le_iff' theorem

{r : ℝ≥0} : ‖x‖₊ ≤ r ↔ ∀ i, ‖x i‖₊ ≤ r

Full source

@[to_additive pi_nnnorm_le_iff]
lemma pi_nnnorm_le_iff' {r : ℝ≥0} : ‖x‖₊‖x‖₊ ≤ r ↔ ∀ i, ‖x i‖₊ ≤ r :=
  pi_norm_le_iff_of_nonneg' r.coe_nonneg

Componentwise Supremum Norm Bound: $\|x\|_{\text{sup}} \leq r \leftrightarrow \forall i, \|x_i\| \leq r$

Informal description

For any nonnegative real number $r$ in the extended nonnegative reals $\mathbb{R}_{\geq 0}$ and any element $x$ in a product of normed groups, the supremum norm $\|x\|_{\text{sup}} \leq r$ if and only if for every index $i$, the norm of the $i$-th component satisfies $\|x_i\| \leq r$.

pi_norm_le_iff_of_nonempty' theorem

[Nonempty ι] : ‖f‖ ≤ r ↔ ∀ b, ‖f b‖ ≤ r

Full source

@[to_additive pi_norm_le_iff_of_nonempty]
lemma pi_norm_le_iff_of_nonempty' [Nonempty ι] : ‖f‖‖f‖ ≤ r ↔ ∀ b, ‖f b‖ ≤ r := by
  by_cases hr : 0 ≤ r
  · exact pi_norm_le_iff_of_nonneg' hr
  · exact
      iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
        hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

Norm Bound in Product Space via Componentwise Bounds (Nonempty Index Case)

Informal description

For a nonempty index set $\iota$ and any real number $r$, the norm of a function $f$ in the product space $\prod_{i \in \iota} G_i$ satisfies $\|f\| \leq r$ if and only if for every index $b \in \iota$, the norm of the component $\|f(b)\| \leq r$.

pi_norm_lt_iff' theorem

(hr : 0 < r) : ‖x‖ < r ↔ ∀ i, ‖x i‖ < r

Full source

/-- The seminorm of an element in a product space is `< r` if and only if the norm of each
component is. -/
@[to_additive pi_norm_lt_iff "The seminorm of an element in a product space is `< r` if and only
if the norm of each component is."]
lemma pi_norm_lt_iff' (hr : 0 < r) : ‖x‖‖x‖ < r ↔ ∀ i, ‖x i‖ < r := by
  simp only [← dist_one_right, dist_pi_lt_iff hr, Pi.one_apply]

Componentwise Norm Bound in Product Space: $\|x\| < r \leftrightarrow \forall i, \|x_i\| < r$

Informal description

For any family of seminormed groups $(G_i)_{i \in I}$ and any positive real number $r > 0$, the norm of an element $x$ in the product space $\prod_{i \in I} G_i$ satisfies $\|x\| < r$ if and only if $\|x_i\| < r$ for every component $x_i$ in $G_i$.

pi_nnnorm_lt_iff' theorem

{r : ℝ≥0} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ i, ‖x i‖₊ < r

Full source

@[to_additive pi_nnnorm_lt_iff]
lemma pi_nnnorm_lt_iff' {r : ℝ≥0} (hr : 0 < r) : ‖x‖₊‖x‖₊ < r ↔ ∀ i, ‖x i‖₊ < r :=
  pi_norm_lt_iff' hr

Componentwise Non-Negative Norm Bound in Product Space: $\|x\|_{\mathbb{R}_{\geq 0}} < r \leftrightarrow \forall i, \|x_i\|_{\mathbb{R}_{\geq 0}} < r$

Informal description

For any family of seminormed groups $(G_i)_{i \in I}$ and any positive real number $r > 0$, the non-negative norm of an element $x$ in the product space $\prod_{i \in I} G_i$ satisfies $\|x\|_{\mathbb{R}_{\geq 0}} < r$ if and only if $\|x_i\|_{\mathbb{R}_{\geq 0}} < r$ for every component $x_i$ in $G_i$.

norm_le_pi_norm' theorem

(i : ι) : ‖f i‖ ≤ ‖f‖

Full source

@[to_additive norm_le_pi_norm]
lemma norm_le_pi_norm' (i : ι) : ‖f i‖ ≤ ‖f‖ :=
  (pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).1 le_rfl i

Componentwise Norm Bound in Product Space: $\|f_i\| \leq \|f\|$

Informal description

For any element $f$ in the product of normed groups $\prod_{i \in \iota} G_i$ and any index $i \in \iota$, the norm of the $i$-th component $\|f(i)\|$ is bounded above by the norm of $f$, i.e., $\|f(i)\| \leq \|f\|$.

nnnorm_le_pi_nnnorm' theorem

(i : ι) : ‖f i‖₊ ≤ ‖f‖₊

Full source

@[to_additive nnnorm_le_pi_nnnorm]
lemma nnnorm_le_pi_nnnorm' (i : ι) : ‖f i‖₊ ≤ ‖f‖₊ :=
  norm_le_pi_norm' _ i

Componentwise Non-Negative Norm Bound in Product Space: $\|f_i\|_{\mathbb{R}_{\geq 0}} \leq \|f\|_{\mathbb{R}_{\geq 0}}$

Informal description

For any element $f$ in the product of normed groups $\prod_{i \in \iota} G_i$ and any index $i \in \iota$, the non-negative norm of the $i$-th component $\|f(i)\|_{\mathbb{R}_{\geq 0}}$ is bounded above by the non-negative norm of $f$, i.e., $\|f(i)\|_{\mathbb{R}_{\geq 0}} \leq \|f\|_{\mathbb{R}_{\geq 0}}$.

pi_norm_const_le' theorem

(a : E) : ‖fun _ : ι => a‖ ≤ ‖a‖

Full source

@[to_additive pi_norm_const_le]
lemma pi_norm_const_le' (a : E) : ‖fun _ : ι => a‖ ≤ ‖a‖ :=
  (pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).2 fun _ => le_rfl

Norm of Constant Function Bounded by Element Norm in Product Space

Informal description

For any element $a$ in a normed group $E$, the norm of the constant function $\lambda \_ \mapsto a$ on any index set $\iota$ is bounded above by the norm of $a$, i.e., \[ \left\| \lambda \_ \mapsto a \right\| \leq \|a\|. \]

pi_nnnorm_const_le' theorem

(a : E) : ‖fun _ : ι => a‖₊ ≤ ‖a‖₊

Full source

@[to_additive pi_nnnorm_const_le]
lemma pi_nnnorm_const_le' (a : E) : ‖fun _ : ι => a‖₊ ≤ ‖a‖₊ :=
  pi_norm_const_le' _

Seminorm of Constant Function Bounded by Element Seminorm in Product Space

Informal description

For any element $a$ in a normed group $E$, the seminorm (with respect to the nonnegative reals) of the constant function $\lambda \_ \mapsto a$ on any index set $\iota$ is bounded above by the seminorm of $a$, i.e., \[ \left\| \lambda \_ \mapsto a \right\|_+ \leq \|a\|_+. \]

pi_norm_const' theorem

[Nonempty ι] (a : E) : ‖fun _i : ι => a‖ = ‖a‖

Full source

@[to_additive (attr := simp) pi_norm_const]
lemma pi_norm_const' [Nonempty ι] (a : E) : ‖fun _i : ι => a‖ = ‖a‖ := by
  simpa only [← dist_one_right] using dist_pi_const a 1

Norm of Constant Function Equals Norm of Element in Product Space

Informal description

For a nonempty index set $\iota$ and an element $a$ in a normed group $E$, the supremum norm of the constant function $\lambda i \mapsto a$ is equal to the norm of $a$, i.e., \[ \left\| \lambda i \mapsto a \right\| = \|a\|. \]

pi_nnnorm_const' theorem

[Nonempty ι] (a : E) : ‖fun _i : ι => a‖₊ = ‖a‖₊

Full source

@[to_additive (attr := simp) pi_nnnorm_const]
lemma pi_nnnorm_const' [Nonempty ι] (a : E) : ‖fun _i : ι => a‖₊ = ‖a‖₊ :=
  NNReal.eq <| pi_norm_const' a

Equality of Seminorms for Constant Function in Product Space

Informal description

For a nonempty index set $\iota$ and an element $a$ in a normed group $E$, the supremum seminorm (with respect to the nonnegative reals) of the constant function $\lambda i \mapsto a$ is equal to the seminorm of $a$, i.e., \[ \left\| \lambda i \mapsto a \right\|_+ = \|a\|_+. \]

Pi.sum_norm_apply_le_norm' theorem

: ∑ i, ‖f i‖ ≤ Fintype.card ι • ‖f‖

Full source

/-- The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality. -/
@[to_additive Pi.sum_norm_apply_le_norm "The $L^1$ norm is less than the $L^\\infty$ norm scaled by
the cardinality."]
lemma Pi.sum_norm_apply_le_norm' : ∑ i, ‖f i‖ ≤ Fintype.card ι • ‖f‖ :=
  Finset.sum_le_card_nsmul _ _ _ fun i _hi => norm_le_pi_norm' _ i

Sum of Component Norms Bounded by Cardinality Times Supremum Norm: $\sum \|f_i\| \leq |\iota| \cdot \|f\|$

Informal description

For any finite index set $\iota$ and any element $f$ in the product of normed groups $\prod_{i \in \iota} G_i$, the sum of the norms of the components $\sum_{i} \|f(i)\|$ is bounded above by the cardinality of $\iota$ multiplied by the supremum norm of $f$, i.e., \[ \sum_{i \in \iota} \|f(i)\| \leq |\iota| \cdot \|f\|. \]

Pi.sum_nnnorm_apply_le_nnnorm' theorem

: ∑ i, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊

Full source

/-- The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality. -/
@[to_additive Pi.sum_nnnorm_apply_le_nnnorm "The $L^1$ norm is less than the $L^\\infty$ norm
scaled by the cardinality."]
lemma Pi.sum_nnnorm_apply_le_nnnorm' : ∑ i, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊ :=
  (NNReal.coe_sum ..).trans_le <| Pi.sum_norm_apply_le_norm' _

Sum of Nonnegative Component Norms Bounded by Cardinality Times Nonnegative Supremum Norm: $\sum \|f_i\|_+ \leq |\iota| \cdot \|f\|_+$

Informal description

For any finite index set $\iota$ and any element $f$ in the product of normed groups $\prod_{i \in \iota} G_i$, the sum of the nonnegative norms of the components $\sum_{i} \|f(i)\|_+$ is bounded above by the cardinality of $\iota$ multiplied by the nonnegative supremum norm of $f$, i.e., \[ \sum_{i \in \iota} \|f(i)\|_+ \leq |\iota| \cdot \|f\|_+. \]

Pi.seminormedCommGroup instance

[∀ i, SeminormedCommGroup (G i)] : SeminormedCommGroup (∀ i, G i)

Full source

/-- Finite product of seminormed groups, using the sup norm. -/
@[to_additive "Finite product of seminormed groups, using the sup norm."]
instance Pi.seminormedCommGroup [∀ i, SeminormedCommGroup (G i)] : SeminormedCommGroup (∀ i, G i) :=
  { Pi.seminormedGroup with
    mul_comm := mul_comm }

Commutative Seminormed Group Structure on Product Types with Supremum Norm

Informal description

For any family of commutative seminormed groups $(G_i)_{i \in I}$, the product type $\prod_{i \in I} G_i$ is also a commutative seminormed group with the supremum norm $\|f\| = \sup_{i \in I} \|f(i)\|$.

Pi.normedGroup instance

[∀ i, NormedGroup (G i)] : NormedGroup (∀ i, G i)

Full source

/-- Finite product of normed groups, using the sup norm. -/
@[to_additive "Finite product of seminormed groups, using the sup norm."]
instance Pi.normedGroup [∀ i, NormedGroup (G i)] : NormedGroup (∀ i, G i) :=
  { Pi.seminormedGroup with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Group Structure on Product Types with Supremum Norm

Informal description

For any family of normed groups $(G_i)_{i \in I}$, the product type $\prod_{i \in I} G_i$ is also a normed group with the supremum norm $\|f\| = \sup_{i \in I} \|f(i)\|$.

Pi.normedCommGroup instance

[∀ i, NormedCommGroup (G i)] : NormedCommGroup (∀ i, G i)

Full source

/-- Finite product of normed groups, using the sup norm. -/
@[to_additive "Finite product of seminormed groups, using the sup norm."]
instance Pi.normedCommGroup [∀ i, NormedCommGroup (G i)] : NormedCommGroup (∀ i, G i) :=
  { Pi.seminormedGroup with
    mul_comm := mul_comm
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Normed Commutative Group Structure on Product Types with Supremum Norm

Informal description

For any family of normed commutative groups $(G_i)_{i \in I}$, the product type $\prod_{i \in I} G_i$ is also a normed commutative group with the supremum norm $\|f\| = \sup_{i \in I} \|f(i)\|$.

Pi.nnnorm_single theorem

[DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖Pi.single i y‖₊ = ‖y‖₊

Full source

theorem Pi.nnnorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) :
    ‖Pi.single i y‖₊ = ‖y‖₊ := by
  have H : ∀ b, ‖single i y b‖₊ = single (f := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
    intro b
    refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
    simp
  simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

Non-Negative Norm of Single Function in Product of Normed Groups

Informal description

For a finite product of normed additive commutative groups $(G_i)_{i \in \iota}$ and a fixed index $i \in \iota$, the non-negative norm of the function `Pi.single i y` (which is $y$ at index $i$ and $0$ elsewhere) equals the non-negative norm of $y$, i.e., $\|\text{Pi.single } i \, y\|_+ = \|y\|_+$.

Pi.enorm_single theorem

[DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖Pi.single i y‖ₑ = ‖y‖ₑ

Full source

lemma Pi.enorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) :
    ‖Pi.single i y‖ₑ = ‖y‖ₑ := by simp [enorm, Pi.nnnorm_single]

Extended Norm of Single Function in Product of Normed Groups

Informal description

For a finite product of normed additive commutative groups $(G_i)_{i \in \iota}$ and a fixed index $i \in \iota$, the extended norm of the function `Pi.single i y` (which is $y$ at index $i$ and $0$ elsewhere) equals the extended norm of $y$, i.e., $\|\text{Pi.single } i \, y\|_e = \|y\|_e$.

Pi.norm_single theorem

[DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖Pi.single i y‖ = ‖y‖

Full source

theorem Pi.norm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) :
    ‖Pi.single i y‖ = ‖y‖ :=
  congr_arg Subtype.val <| Pi.nnnorm_single y

Norm of Single Function in Product of Normed Groups Equals Norm of Element

Informal description

For a finite product of normed additive commutative groups $(G_i)_{i \in \iota}$ and a fixed index $i \in \iota$, the norm of the function $\text{Pi.single } i \, y$ (which is $y$ at index $i$ and $0$ elsewhere) equals the norm of $y$, i.e., $\|\text{Pi.single } i \, y\| = \|y\|$.

MulOpposite.instSeminormedAddGroup instance

[SeminormedAddGroup E] : SeminormedAddGroup Eᵐᵒᵖ

Full source

/-- 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.
-/
instance instSeminormedAddGroup [SeminormedAddGroup E] : SeminormedAddGroup Eᵐᵒᵖ where
  __ := instPseudoMetricSpace
  norm x := ‖x.unop‖
  dist_eq _ _ := dist_eq_norm _ _

Seminormed Additive Group Structure on the Multiplicative Opposite

Informal description

For any seminormed additive group $E$, the multiplicative opposite $E^\text{op}$ inherits a seminormed additive group structure, where the norm of an element $\text{op}(x)$ is equal to the norm of $x$ in $E$.

MulOpposite.norm_op theorem

[SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖ = ‖a‖

Full source

lemma norm_op [SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖ = ‖a‖ := rfl

Norm Preservation under Multiplicative Opposite

Informal description

For any seminormed additive group $E$ and any element $a \in E$, the norm of the multiplicative opposite $\text{op}(a) \in E^\text{op}$ is equal to the norm of $a$, i.e., $\|\text{op}(a)\| = \|a\|$.

MulOpposite.norm_unop theorem

[SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖ = ‖a‖

Full source

lemma norm_unop [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖ = ‖a‖ := rfl

Norm Preservation under Projection from Multiplicative Opposite

Informal description

For any seminormed additive group $E$ and any element $a$ in the multiplicative opposite $E^\text{op}$, the norm of the projection of $a$ back to $E$ is equal to the norm of $a$ in $E^\text{op}$. That is, $\|\text{unop}(a)\| = \|a\|$.

MulOpposite.nnnorm_op theorem

[SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖₊ = ‖a‖₊

Full source

lemma nnnorm_op [SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖₊ = ‖a‖₊ := rfl

Seminorm Preservation under Multiplicative Opposite Embedding

Informal description

For any seminormed additive group $E$ and any element $a \in E$, the seminorm of the multiplicative opposite $\text{op}(a)$ in $E^\text{op}$ is equal to the seminorm of $a$ in $E$, i.e., $\|\text{op}(a)\|_+ = \|a\|_+$.

MulOpposite.nnnorm_unop theorem

[SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖₊ = ‖a‖₊

Full source

lemma nnnorm_unop [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖₊ = ‖a‖₊ := rfl

Equality of Seminorms in Multiplicative Opposite and Original Group

Informal description

For any seminormed additive group $E$ and any element $a$ in the multiplicative opposite $E^\text{op}$, the seminorm of the canonical projection $\text{unop}(a)$ in $E$ is equal to the seminorm of $a$ in $E^\text{op}$, i.e., $\|\text{unop}(a)\| = \|a\|$.

MulOpposite.instNormedAddGroup instance

[NormedAddGroup E] : NormedAddGroup Eᵐᵒᵖ

Full source

instance instNormedAddGroup [NormedAddGroup E] : NormedAddGroup Eᵐᵒᵖ where
  __ := instMetricSpace
  __ := instSeminormedAddGroup

Normed Additive Group Structure on the Multiplicative Opposite

Informal description

For any normed additive group $E$, the multiplicative opposite $E^\text{op}$ inherits a normed additive group structure, where the norm of an element $\text{op}(x)$ is equal to the norm of $x$ in $E$.

MulOpposite.instSeminormedAddCommGroup instance

[SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵐᵒᵖ

Full source

instance instSeminormedAddCommGroup [SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵐᵒᵖ where
  dist_eq _ _ := dist_eq_norm _ _

Seminormed Additive Commutative Group Structure on the Multiplicative Opposite

Informal description

For any seminormed additive commutative group $E$, the multiplicative opposite $E^\text{op}$ inherits a seminormed additive commutative group structure, where the norm of an element $\text{op}(x)$ is equal to the norm of $x$ in $E$.

MulOpposite.instNormedAddCommGroup instance

[NormedAddCommGroup E] : NormedAddCommGroup Eᵐᵒᵖ

Full source

instance instNormedAddCommGroup [NormedAddCommGroup E] : NormedAddCommGroup Eᵐᵒᵖ where
  __ := instSeminormedAddCommGroup
  __ := instNormedAddGroup

Normed Additive Commutative Group Structure on the Multiplicative Opposite

Informal description

For any normed additive commutative group $E$, the multiplicative opposite $E^\text{op}$ inherits a normed additive commutative group structure, where the norm of an element $\text{op}(x)$ is equal to the norm of $x$ in $E$.