Product of normed groups and other constructions #

theorem Pi.seminormedAddGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :

↑(Finset.univ.sup fun (b : ι) => nndist (x b) (y b)) = ↑(Finset.univ.sup fun (b : ι) => ‖(x - y) b‖₊)

source

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

SeminormedAddGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.seminormedAddGroup = SeminormedAddGroup.mk ⋯

source

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

SeminormedGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.seminormedGroup = SeminormedGroup.mk ⋯

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem pi_norm_le_iff_of_nonneg {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π 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.

source

theorem pi_norm_le_iff_of_nonneg' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π 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.

source

theorem pi_nnnorm_le_iff {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} :

‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

source

theorem pi_nnnorm_le_iff' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} :

‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

source

theorem pi_norm_le_iff_of_nonempty {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) {r : ℝ} [Nonempty ι] :

‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

source

theorem pi_norm_le_iff_of_nonempty' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) {r : ℝ} [Nonempty ι] :

‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

source

theorem pi_norm_lt_iff {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π 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.

source

theorem pi_norm_lt_iff' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π 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.

source

theorem pi_nnnorm_lt_iff {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) :

‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

source

theorem pi_nnnorm_lt_iff' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) :

‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

source

theorem norm_le_pi_norm {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) :

‖f i‖ ≤ ‖f‖

source

theorem norm_le_pi_norm' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) :

‖f i‖ ≤ ‖f‖

source

theorem nnnorm_le_pi_nnnorm {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) :

‖f i‖₊ ≤ ‖f‖₊

source

theorem nnnorm_le_pi_nnnorm' {ι : Type u_1} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) :

‖f i‖₊ ≤ ‖f‖₊

source

theorem pi_norm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) :

‖fun (x : ι) => a‖ ≤ ‖a‖

source

theorem pi_norm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) :

‖fun (x : ι) => a‖ ≤ ‖a‖

source

theorem pi_nnnorm_const_le {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] (a : E) :

‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

source

theorem pi_nnnorm_const_le' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] (a : E) :

‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

source

@[simp]

theorem pi_norm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :

‖fun (_i : ι) => a‖ = ‖a‖

source

@[simp]

theorem pi_norm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :

‖fun (_i : ι) => a‖ = ‖a‖

source

@[simp]

theorem pi_nnnorm_const {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) :

‖fun (_i : ι) => a‖₊ = ‖a‖₊

source

@[simp]

theorem pi_nnnorm_const' {ι : Type u_1} {E : Type u_2} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) :

‖fun (_i : ι) => a‖₊ = ‖a‖₊

source

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

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

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

source

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

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

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

source

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

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

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

source

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

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

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

source

theorem Pi.seminormedAddCommGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :

dist x y = ‖x - y‖

source

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

SeminormedAddCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.seminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

source

theorem Pi.seminormedAddCommGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → SeminormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :

a + b = b + a

source

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

SeminormedCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.seminormedCommGroup = SeminormedCommGroup.mk ⋯

source

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

NormedAddGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.normedAddGroup = NormedAddGroup.mk ⋯

source

theorem Pi.normedAddGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :

dist x y = ‖x - y‖

source

theorem Pi.normedAddGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] :

∀ {x y : (i : ι) → π i}, dist x y = 0 → x = y

source

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

NormedGroup ((i : ι) → π i)

Finite product of normed groups, using the sup norm.

Equations

Pi.normedGroup = NormedGroup.mk ⋯

source

theorem Pi.normedAddCommGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] :

∀ {x y : (i : ι) → π i}, dist x y = 0 → x = y

source

theorem Pi.normedAddCommGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → NormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :

a + b = b + a

source

theorem Pi.normedAddCommGroup.proof_3 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) :

dist x y = ‖x - y‖

source

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

NormedAddCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

Pi.normedAddCommGroup = NormedAddCommGroup.mk ⋯

source

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

NormedCommGroup ((i : ι) → π i)

Finite product of normed groups, using the sup norm.

Equations

Pi.normedCommGroup = NormedCommGroup.mk ⋯

source

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

‖Pi.single i y‖₊ = ‖y‖₊

source

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

‖Pi.single i y‖ = ‖y‖

Multiplicative opposite #

source

instance MulOpposite.instSeminormedAddGroup {E : Type u_2} [SeminormedAddGroup E] :

SeminormedAddGroup Eᵐᵒᵖ

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