# mathlibdocumentation

analysis.normed.group.basic

# Normed (semi)groups #

In this file we define four classes:

• has_norm, has_nnnorm: auxiliary classes endowing a type α with a function norm : α → ℝ (notation: ∥x∥) and nnnorm : α → ℝ≥0 (notation: ∥x∥₊), respectively;
• semi_normed_group: a seminormed group is an additive group with a norm and a pseudo metric space structures that agree with each other: ∀ x y, dist x y = ∥x - y∥;
• normed_group: a normed group is an additive group with a norm and a metric space structures that agree with each other: ∀ x y, dist x y = ∥x - y∥.

We also prove basic properties of (semi)normed groups and provide some instances.

## Tags #

normed group

@[class]
structure has_norm (E : Type u_6) :
Type u_6
• norm : E →

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ∥x∥. This class is designed to be extended in more interesting classes specifying the properties of the norm.

Instances of this typeclass
Instances of other typeclasses for has_norm
• has_norm.has_sizeof_inst
@[class]
structure semi_normed_group (E : Type u_6) :
Type u_6
• to_has_norm :
• to_pseudo_metric_space :
• dist_eq : ∀ (x y : E), = x - y

A seminormed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines a pseudometric space structure.

Instances of this typeclass
Instances of other typeclasses for semi_normed_group
• semi_normed_group.has_sizeof_inst
@[class]
structure normed_group (E : Type u_6) :
Type u_6
• to_has_norm :
• to_metric_space :
• dist_eq : ∀ (x y : E), = x - y

A normed group is an additive group endowed with a norm for which dist x y = ∥x - y∥ defines a metric space structure.

Instances of this typeclass
Instances of other typeclasses for normed_group
• normed_group.has_sizeof_inst
@[protected, instance]
def normed_group.to_semi_normed_group {E : Type u_3} [h : normed_group E] :

A normed group is a seminormed group.

Equations
def semi_normed_group.of_add_dist {E : Type u_3} [has_norm E] (H1 : ∀ (x : E), x = ) (H2 : ∀ (x y z : E), has_dist.dist (x + z) (y + z)) :

Construct a seminormed group from a translation invariant pseudodistance.

Equations
def semi_normed_group.of_add_dist' {E : Type u_3} [has_norm E] (H1 : ∀ (x : E), x = ) (H2 : ∀ (x y z : E), has_dist.dist (x + z) (y + z) ) :

Construct a seminormed group from a translation invariant pseudodistance

Equations
structure semi_normed_group.core (E : Type u_6) [has_norm E] :
Prop

A seminormed group can be built from a seminorm that satisfies algebraic properties. This is formalised in this structure.

def semi_normed_group.of_core (E : Type u_1) [has_norm E] (C : semi_normed_group.core E) :

Constructing a seminormed group from core properties of a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing uniform_space instance on E).

Equations
@[protected, instance]
Equations
@[simp]
theorem punit.norm_eq_zero (r : punit) :
@[protected, instance]
noncomputable def real.normed_group  :
Equations
theorem real.norm_eq_abs (r : ) :
theorem dist_eq_norm {E : Type u_3} (g h : E) :
= g - h
theorem dist_eq_norm' {E : Type u_3} (g h : E) :
= h - g
@[simp]
theorem dist_zero_right {E : Type u_3} (g : E) :
@[simp]
theorem dist_zero_left {E : Type u_3}  :
theorem tendsto_norm_cocompact_at_top {E : Type u_3} [proper_space E] :
theorem norm_sub_rev {E : Type u_3} (g h : E) :
g - h = h - g
@[simp]
theorem norm_neg {E : Type u_3} (g : E) :
@[simp]
theorem dist_add_left {E : Type u_3} (g h₁ h₂ : E) :
has_dist.dist (g + h₁) (g + h₂) = h₂
@[simp]
theorem dist_add_right {E : Type u_3} (g₁ g₂ h : E) :
has_dist.dist (g₁ + h) (g₂ + h) = g₂
theorem dist_neg {E : Type u_3} (x y : E) :
y = (-y)
@[simp]
theorem dist_neg_neg {E : Type u_3} (g h : E) :
(-h) =
@[simp]
theorem dist_sub_left {E : Type u_3} (g h₁ h₂ : E) :
has_dist.dist (g - h₁) (g - h₂) = h₂
@[simp]
theorem dist_sub_right {E : Type u_3} (g₁ g₂ h : E) :
has_dist.dist (g₁ - h) (g₂ - h) = g₂
@[simp]
theorem dist_self_add_right {E : Type u_3} (g h : E) :
(g + h) = h
@[simp]
theorem dist_self_add_left {E : Type u_3} (g h : E) :
@[simp]
theorem dist_self_sub_right {E : Type u_3} (g h : E) :
(g - h) = h
@[simp]
theorem dist_self_sub_left {E : Type u_3} (g h : E) :
theorem filter.tendsto_neg_cobounded {E : Type u_3}  :

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

theorem norm_add_le {E : Type u_3} (g h : E) :

Triangle inequality for the norm.

theorem norm_add_le_of_le {E : Type u_3} {g₁ g₂ : E} {n₁ n₂ : } (H₁ : g₁ n₁) (H₂ : g₂ n₂) :
g₁ + g₂ n₁ + n₂
theorem dist_add_add_le {E : Type u_3} (g₁ g₂ h₁ h₂ : E) :
has_dist.dist (g₁ + g₂) (h₁ + h₂) h₁ + h₂
theorem dist_add_add_le_of_le {E : Type u_3} {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : } (H₁ : h₁ d₁) (H₂ : h₂ d₂) :
has_dist.dist (g₁ + g₂) (h₁ + h₂) d₁ + d₂
theorem dist_sub_sub_le {E : Type u_3} (g₁ g₂ h₁ h₂ : E) :
has_dist.dist (g₁ - g₂) (h₁ - h₂) h₁ + h₂
theorem dist_sub_sub_le_of_le {E : Type u_3} {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : } (H₁ : h₁ d₁) (H₂ : h₂ d₂) :
has_dist.dist (g₁ - g₂) (h₁ - h₂) d₁ + d₂
theorem abs_dist_sub_le_dist_add_add {E : Type u_3} (g₁ g₂ h₁ h₂ : E) :
| h₁ - h₂| has_dist.dist (g₁ + g₂) (h₁ + h₂)
@[simp]
theorem norm_nonneg {E : Type u_3} (g : E) :
@[simp]
theorem norm_zero {E : Type u_3}  :
theorem ne_zero_of_norm_ne_zero {E : Type u_3} {g : E} :
g 0g 0
theorem norm_of_subsingleton {E : Type u_3} [subsingleton E] (x : E) :
theorem norm_sum_le {ι : Type u_2} {E : Type u_3} (s : finset ι) (f : ι → E) :
s.sum (λ (i : ι), f i) s.sum (λ (i : ι), f i)
theorem norm_sum_le_of_le {ι : Type u_2} {E : Type u_3} (s : finset ι) {f : ι → E} {n : ι → } (h : ∀ (b : ι), b sf b n b) :
s.sum (λ (b : ι), f b) s.sum (λ (b : ι), n b)
theorem dist_sum_sum_le_of_le {ι : Type u_2} {E : Type u_3} (s : finset ι) {f g : ι → E} {d : ι → } (h : ∀ (b : ι), b shas_dist.dist (f b) (g b) d b) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), g b)) s.sum (λ (b : ι), d b)
theorem dist_sum_sum_le {ι : Type u_2} {E : Type u_3} (s : finset ι) (f g : ι → E) :
has_dist.dist (s.sum (λ (b : ι), f b)) (s.sum (λ (b : ι), g b)) s.sum (λ (b : ι), has_dist.dist (f b) (g b))
theorem norm_sub_le {E : Type u_3} (g h : E) :
theorem norm_sub_le_of_le {E : Type u_3} {g₁ g₂ : E} {n₁ n₂ : } (H₁ : g₁ n₁) (H₂ : g₂ n₂) :
g₁ - g₂ n₁ + n₂
theorem dist_le_norm_add_norm {E : Type u_3} (g h : E) :
theorem abs_norm_sub_norm_le {E : Type u_3} (g h : E) :
theorem norm_sub_norm_le {E : Type u_3} (g h : E) :
theorem dist_norm_norm_le {E : Type u_3} (g h : E) :
theorem norm_le_insert {E : Type u_3} (u v : E) :

The direct path from 0 to v is shorter than the path with u inserted in between.

theorem norm_le_insert' {E : Type u_3} (u v : E) :
theorem ball_eq {E : Type u_3} (y : E) (ε : ) :
ε = {x : E | x - y < ε}
theorem ball_zero_eq {E : Type u_3} (ε : ) :
ε = {x : E | x < ε}
theorem mem_ball_iff_norm {E : Type u_3} {g h : E} {r : } :
h r h - g < r
theorem add_mem_ball_iff_norm {E : Type u_3} {g h : E} {r : } :
g + h r h < r
theorem mem_ball_iff_norm' {E : Type u_3} {g h : E} {r : } :
h r g - h < r
@[simp]
theorem mem_ball_zero_iff {E : Type u_3} {ε : } {x : E} :
x ε x < ε
theorem mem_closed_ball_iff_norm {E : Type u_3} {g h : E} {r : } :
h h - g r
@[simp]
theorem mem_closed_ball_zero_iff {E : Type u_3} {ε : } {x : E} :
theorem add_mem_closed_ball_iff_norm {E : Type u_3} {g h : E} {r : } :
g + h h r
theorem mem_closed_ball_iff_norm' {E : Type u_3} {g h : E} {r : } :
h g - h r
theorem norm_le_of_mem_closed_ball {E : Type u_3} {g h : E} {r : } (H : h ) :
theorem norm_le_norm_add_const_of_dist_le {E : Type u_3} {a b : E} {c : } (h : c) :
theorem norm_lt_of_mem_ball {E : Type u_3} {g h : E} {r : } (H : h r) :
theorem norm_lt_norm_add_const_of_dist_lt {E : Type u_3} {a b : E} {c : } (h : < c) :
theorem bounded_iff_forall_norm_le {E : Type u_3} {s : set E} :
∃ (C : ), ∀ (x : E), x sx C
@[simp]
theorem preimage_add_ball {E : Type u_3} (x y : E) (r : ) :
= metric.ball (x - y) r
@[simp]
theorem preimage_add_closed_ball {E : Type u_3} (x y : E) (r : ) :
@[simp]
theorem mem_sphere_iff_norm {E : Type u_3} (v w : E) (r : ) :
w w - v = r
@[simp]
theorem mem_sphere_zero_iff_norm {E : Type u_3} {w : E} {r : } :
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_3} {r : } (x : r)) :
theorem preimage_add_sphere {E : Type u_3} (x y : E) (r : ) :
= metric.sphere (x - y) r
theorem ne_zero_of_mem_sphere {E : Type u_3} {r : } (hr : r 0) (x : r)) :
x 0
theorem ne_zero_of_mem_unit_sphere {E : Type u_3} (x : 1)) :
x 0
@[protected, instance]
def metric.sphere.has_neg {E : Type u_3} {r : } :

We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.

Equations
@[simp]
theorem coe_neg_sphere {E : Type u_3} {r : } (v : r)) :
@[protected]
def isometric.add_right {E : Type u_3} (x : E) :
E ≃ᵢ E

Addition y ↦ y + x as an isometry.

Equations
@[simp]
theorem isometric.add_right_to_equiv {E : Type u_3} (x : E) :
@[simp]
theorem isometric.coe_add_right {E : Type u_3} (x : E) :
= λ (y : E), y + x
theorem isometric.add_right_apply {E : Type u_3} (x y : E) :
y = y + x
@[simp]
theorem isometric.add_right_symm {E : Type u_3} (x : E) :
@[protected]
def isometric.add_left {E : Type u_3} (x : E) :
E ≃ᵢ E

Addition y ↦ x + y as an isometry.

Equations
@[simp]
theorem isometric.add_left_to_equiv {E : Type u_3} (x : E) :
@[simp]
theorem isometric.coe_add_left {E : Type u_3} (x : E) :
@[simp]
theorem isometric.add_left_symm {E : Type u_3} (x : E) :
@[protected]
def isometric.neg (E : Type u_3)  :
E ≃ᵢ E

Negation x ↦ -x as an isometry.

Equations
@[simp]
theorem isometric.neg_symm {E : Type u_3}  :
@[simp]
theorem isometric.neg_to_equiv {E : Type u_3}  :
@[simp]
theorem isometric.coe_neg {E : Type u_3}  :
theorem normed_group.tendsto_nhds_zero {α : Type u_1} {E : Type u_3} {f : α → E} {l : filter α} :
(nhds 0) ∀ (ε : ), ε > 0(∀ᶠ (x : α) in l, f x < ε)
theorem normed_group.tendsto_nhds_nhds {E : Type u_3} {F : Type u_4} {f : E → F} {x : E} {y : F} :
(nhds x) (nhds y) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x' : E), x' - x < δf x' - y < ε)
theorem normed_group.cauchy_seq_iff {α : Type u_1} {E : Type u_3} [nonempty α] {u : α → E} :
∀ (ε : ), ε > 0(∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m - u n < ε)
theorem normed_group.nhds_basis_norm_lt {E : Type u_3} (x : E) :
(nhds x).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {y : E | y - x < ε})
theorem normed_group.nhds_zero_basis_norm_lt {E : Type u_3}  :
(nhds 0).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {y : E | y < ε})
theorem normed_group.uniformity_basis_dist {E : Type u_3}  :
(uniformity E).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {p : E × E | p.fst - p.snd < ε})
theorem add_monoid_hom.lipschitz_of_bound {E : Type u_3} {F : Type u_4} (f : E →+ F) (C : ) (h : ∀ (x : E), f x C * x) :

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ∥f x∥ ≤ C * ∥x∥. The analogous condition for a linear map of (semi)normed spaces is in normed_space.operator_norm.

theorem lipschitz_on_with_iff_norm_sub_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} {s : set E} :
s ∀ (x : E), x s∀ (y : E), y sf x - f y C * x - y
theorem lipschitz_on_with.norm_sub_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} {s : set E} (h : s) {x y : E} (x_in : x s) (y_in : y s) :
f x - f y C * x - y
theorem lipschitz_on_with.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} {s : set E} (h : s) {x y : E} (x_in : x s) (y_in : y s) {d : } (hd : x - y d) :
f x - f y C * d
theorem lipschitz_with_iff_norm_sub_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} :
∀ (x y : E), f x - f y C * x - y
theorem lipschitz_with.norm_sub_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} :
∀ (x y : E), f x - f y C * x - y

Alias of the forward direction of lipschitz_with_iff_norm_sub_le.

theorem lipschitz_with.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} {f : E → F} {C : nnreal} (h : f) {x y : E} {d : } (hd : x - y d) :
f x - f y C * d
theorem add_monoid_hom.continuous_of_bound {E : Type u_3} {F : Type u_4} (f : E →+ F) (C : ) (h : ∀ (x : E), f x C * x) :

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ∥f x∥ ≤ C * ∥x∥. The analogous condition for a linear map of normed spaces is in normed_space.operator_norm.

theorem is_compact.exists_bound_of_continuous_on {α : Type u_1} {E : Type u_3} {s : set α} (hs : is_compact s) {f : α → E} (hf : s) :
∃ (C : ), ∀ (x : α), x sf x C
theorem add_monoid_hom.isometry_iff_norm {E : Type u_3} {F : Type u_4} (f : E →+ F) :
∀ (x : E), f x = x
theorem add_monoid_hom.isometry_of_norm {E : Type u_3} {F : Type u_4} (f : E →+ F) (hf : ∀ (x : E), f x = x) :
theorem controlled_sum_of_mem_closure {E : Type u_3} {s : add_subgroup E} {g : E} (hg : g ) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (v : → E), filter.tendsto (λ (n : ), (finset.range (n + 1)).sum (λ (i : ), v i)) filter.at_top (nhds g) (∀ (n : ), v n s) v 0 - g < b 0 ∀ (n : ), n > 0v n < b n
theorem controlled_sum_of_mem_closure_range {E : Type u_3} {F : Type u_4} {j : E →+ F} {h : F} (Hh : h closure (j.range)) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (g : → E), filter.tendsto (λ (n : ), (finset.range (n + 1)).sum (λ (i : ), j (g i))) filter.at_top (nhds h) j (g 0) - h < b 0 ∀ (n : ), n > 0j (g n) < b n
@[class]
structure has_nnnorm (E : Type u_6) :
Type u_6

Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ∥x∥₊.

Instances of this typeclass
Instances of other typeclasses for has_nnnorm
• has_nnnorm.has_sizeof_inst
@[protected, instance]
def semi_normed_group.to_has_nnnorm {E : Type u_3}  :
Equations
@[simp, norm_cast]
theorem coe_nnnorm {E : Type u_3} (a : E) :
@[simp]
theorem coe_comp_nnnorm {E : Type u_3}  :
theorem norm_to_nnreal {E : Type u_3} {a : E} :
theorem nndist_eq_nnnorm {E : Type u_3} (a b : E) :
@[simp]
theorem nnnorm_zero {E : Type u_3}  :
theorem ne_zero_of_nnnorm_ne_zero {E : Type u_3} {g : E} :
g∥₊ 0g 0
theorem nnnorm_add_le {E : Type u_3} (g h : E) :
@[simp]
theorem nnnorm_neg {E : Type u_3} (g : E) :
theorem nndist_nnnorm_nnnorm_le {E : Type u_3} (g h : E) :
theorem nnnorm_le_insert {E : Type u_3} (u v : E) :

The direct path from 0 to v is shorter than the path with u inserted in between.

theorem nnnorm_le_insert' {E : Type u_3} (u v : E) :
theorem of_real_norm_eq_coe_nnnorm {E : Type u_3} (x : E) :
theorem edist_eq_coe_nnnorm_sub {E : Type u_3} (x y : E) :
theorem edist_eq_coe_nnnorm {E : Type u_3} (x : E) :
theorem mem_emetric_ball_zero_iff {E : Type u_3} {x : E} {r : ennreal} :
theorem nndist_add_add_le {E : Type u_3} (g₁ g₂ h₁ h₂ : E) :
has_nndist.nndist (g₁ + g₂) (h₁ + h₂) h₁ + h₂
theorem edist_add_add_le {E : Type u_3} (g₁ g₂ h₁ h₂ : E) :
has_edist.edist (g₁ + g₂) (h₁ + h₂) h₁ + h₂
@[simp]
theorem edist_add_left {E : Type u_3} (g h₁ h₂ : E) :
has_edist.edist (g + h₁) (g + h₂) = h₂
@[simp]
theorem edist_add_right {E : Type u_3} (g₁ g₂ h : E) :
has_edist.edist (g₁ + h) (g₂ + h) = g₂
theorem edist_neg {E : Type u_3} (x y : E) :
y = (-y)
@[simp]
theorem edist_neg_neg {E : Type u_3} (x y : E) :
(-y) =
@[simp]
theorem edist_sub_left {E : Type u_3} (g h₁ h₂ : E) :
has_edist.edist (g - h₁) (g - h₂) = h₂
@[simp]
theorem edist_sub_right {E : Type u_3} (g₁ g₂ h : E) :
has_edist.edist (g₁ - h) (g₂ - h) = g₂
theorem nnnorm_sum_le {ι : Type u_2} {E : Type u_3} (s : finset ι) (f : ι → E) :
s.sum (λ (a : ι), f a)∥₊ s.sum (λ (a : ι), f a∥₊)
theorem nnnorm_sum_le_of_le {ι : Type u_2} {E : Type u_3} (s : finset ι) {f : ι → E} {n : ι → nnreal} (h : ∀ (b : ι), b sf b∥₊ n b) :
s.sum (λ (b : ι), f b)∥₊ s.sum (λ (b : ι), n b)
theorem add_monoid_hom.lipschitz_of_bound_nnnorm {E : Type u_3} {F : Type u_4} (f : E →+ F) (C : nnreal) (h : ∀ (x : E), f x∥₊ C * x∥₊) :
theorem lipschitz_with.neg {α : Type u_1} {E : Type u_3} {K : nnreal} {f : α → E} (hf : f) :
(λ (x : α), -f x)
theorem lipschitz_with.add {α : Type u_1} {E : Type u_3} {Kf Kg : nnreal} {f g : α → E} (hf : f) (hg : g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
theorem lipschitz_with.sub {α : Type u_1} {E : Type u_3} {Kf Kg : nnreal} {f g : α → E} (hf : f) (hg : g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
theorem antilipschitz_with.add_lipschitz_with {α : Type u_1} {E : Type u_3} {Kf Kg : nnreal} {f g : α → E} (hf : f) (hg : g) (hK : Kg < Kf⁻¹) :
antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ (x : α), f x + g x)
theorem antilipschitz_with.add_sub_lipschitz_with {α : Type u_1} {E : Type u_3} {Kf Kg : nnreal} {f g : α → E} (hf : f) (hg : (g - f)) (hK : Kg < Kf⁻¹) :
theorem antilipschitz_with.le_mul_norm_sub {E : Type u_3} {F : Type u_4} {K : nnreal} {f : E → F} (hf : f) (x y : E) :
x - y K * f x - f y
def semi_normed_group.induced {F : Type u_4} {E : Type u_1} (f : E →+ F) :

A group homomorphism from an add_comm_group to a semi_normed_group induces a semi_normed_group structure on the domain.

Equations
@[protected, instance]

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
@[simp]
theorem add_subgroup.coe_norm {E : Type u_1} {s : add_subgroup E} (x : s) :

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

@[norm_cast]
theorem add_subgroup.norm_coe {E : Type u_1} {s : add_subgroup E} (x : s) :

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma add_subgroup.coe_norm for use by norm_cast.

@[protected, instance]
def submodule.semi_normed_group {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} {_x_1 : E} (s : E) :

A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations
@[simp]
theorem submodule.coe_norm {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} {_x_1 : E} {s : E} (x : s) :

If x is an element of a submodule s of a normed group E, its norm in s is equal to its norm in E.

@[norm_cast]
theorem submodule.norm_coe {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} {_x_1 : E} {s : E} (x : s) :

If x is an element of a submodule s of a normed group E, its norm in E is equal to its norm in s.

This is a reversed version of the simp lemma submodule.coe_norm for use by norm_cast.

@[protected, instance]
def ulift.semi_normed_group {E : Type u_3}  :
Equations
theorem ulift.norm_def {E : Type u_3} (x : ulift E) :
theorem ulift.nnnorm_def {E : Type u_3} (x : ulift E) :
@[simp]
theorem ulift.norm_up {E : Type u_3} (x : E) :
@[simp]
theorem ulift.nnnorm_up {E : Type u_3} (x : E) :
@[protected, instance]
noncomputable def prod.semi_normed_group {E : Type u_3} {F : Type u_4}  :

seminormed group instance on the product of two seminormed groups, using the sup norm.

Equations
theorem prod.norm_def {E : Type u_3} {F : Type u_4} (x : E × F) :
theorem prod.nnnorm_def {E : Type u_3} {F : Type u_4} (x : E × F) :
theorem norm_fst_le {E : Type u_3} {F : Type u_4} (x : E × F) :
theorem norm_snd_le {E : Type u_3} {F : Type u_4} (x : E × F) :
theorem norm_prod_le_iff {E : Type u_3} {F : Type u_4} {x : E × F} {r : } :
@[protected, instance]
noncomputable def pi.semi_normed_group {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] :
semi_normed_group (Π (i : ι), π i)

seminormed group instance on the product of finitely many seminormed groups, using the sup norm.

Equations
theorem pi.norm_def {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (f : Π (i : ι), π i) :
f = (finset.univ.sup (λ (b : ι), f b∥₊))
theorem pi.nnnorm_def {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (f : Π (i : ι), π i) :
f∥₊ = finset.univ.sup (λ (b : ι), f b∥₊)
theorem pi_norm_le_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : } (hr : 0 r) {x : Π (i : ι), π i} :
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_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : nnreal} {x : Π (i : ι), π i} :
x∥₊ r ∀ (i : ι), x i∥₊ r
theorem pi_norm_lt_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : } (hr : 0 < r) {x : Π (i : ι), π i} :
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_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] {r : nnreal} (hr : 0 < r) {x : Π (i : ι), π i} :
x∥₊ < r ∀ (i : ι), x i∥₊ < r
theorem norm_le_pi_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) (i : ι) :
theorem nnnorm_le_pi_nnnorm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) (i : ι) :
@[simp]
theorem pi_norm_const {ι : Type u_2} {E : Type u_3} [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnnorm_const {ι : Type u_2} {E : Type u_3} [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a)∥₊ = a∥₊
theorem pi.sum_norm_apply_le_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), x 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_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group (π i)] (x : Π (i : ι), π i) :
finset.univ.sum (λ (i : ι), x i∥₊)

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

theorem tendsto_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} {f : α → E} {a : filter α} {b : E} :
(nhds b) filter.tendsto (λ (e : α), f e - b) a (nhds 0)
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} {f : α → E} {a : filter α} :
(nhds 0) filter.tendsto (λ (e : α), f e) a (nhds 0)
theorem squeeze_zero_norm' {α : Type u_1} {E : Type u_3} {f : α → E} {g : α → } {t₀ : filter α} (h : ∀ᶠ (n : α) in t₀, f n g n) (h' : t₀ (nhds 0)) :
t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is eventually bounded by a real function g which tends to 0, then f tends to 0. In this pair of lemmas (squeeze_zero_norm' and squeeze_zero_norm), following a convention of similar lemmas in topology.metric_space.basic and topology.algebra.order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

theorem squeeze_zero_norm {α : Type u_1} {E : Type u_3} {f : α → E} {g : α → } {t₀ : filter α} (h : ∀ (n : α), f n g n) (h' : t₀ (nhds 0)) :
t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of f is bounded by a real function g which tends to 0, then f tends to 0.

theorem tendsto_norm_sub_self {E : Type u_3} (x : E) :
filter.tendsto (λ (g : E), g - x) (nhds x) (nhds 0)
theorem tendsto_norm {E : Type u_3} {x : E} :
filter.tendsto (λ (g : E), g) (nhds x) (nhds x)
theorem tendsto_norm_zero {E : Type u_3}  :
filter.tendsto (λ (g : E), g) (nhds 0) (nhds 0)
@[continuity]
theorem continuous_norm {E : Type u_3}  :
continuous (λ (g : E), g)
@[continuity]
theorem continuous_nnnorm {E : Type u_3}  :
continuous (λ (a : E), a∥₊)
theorem lipschitz_with_one_norm {E : Type u_3}  :
theorem lipschitz_with_one_nnnorm {E : Type u_3}  :
theorem uniform_continuous_norm {E : Type u_3}  :
theorem uniform_continuous_nnnorm {E : Type u_3}  :
theorem filter.tendsto.op_zero_is_bounded_under_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} {f : α → E} {g : α → F} {l : filter α} (hf : (nhds 0)) (hg : ) (op : E → F → G) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ∥op x y∥ ≤ A * ∥x∥ * ∥y∥ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem filter.tendsto.op_zero_is_bounded_under_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} {f : α → E} {g : α → F} {l : filter α} (hf : (nhds 0)) (hg : ) (op : E → F → G) (h_op : ∀ (x : E) (y : F), op x y x * y) :
filter.tendsto (λ (x : α), op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ∥op x y∥ ≤ ∥x∥ * ∥y∥ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem filter.tendsto.norm {α : Type u_1} {E : Type u_3} {l : filter α} {f : α → E} {a : E} (h : (nhds a)) :
filter.tendsto (λ (x : α), f x) l (nhds a)
theorem filter.tendsto.nnnorm {α : Type u_1} {E : Type u_3} {l : filter α} {f : α → E} {a : E} (h : (nhds a)) :
filter.tendsto (λ (x : α), f x∥₊) l (nhds a∥₊)
theorem continuous.norm {α : Type u_1} {E : Type u_3} {f : α → E} (h : continuous f) :
continuous (λ (x : α), f x)
theorem continuous.nnnorm {α : Type u_1} {E : Type u_3} {f : α → E} (h : continuous f) :
continuous (λ (x : α), f x∥₊)
theorem continuous_at.norm {α : Type u_1} {E : Type u_3} {f : α → E} {a : α} (h : a) :
continuous_at (λ (x : α), f x) a
theorem continuous_at.nnnorm {α : Type u_1} {E : Type u_3} {f : α → E} {a : α} (h : a) :
continuous_at (λ (x : α), f x∥₊) a
theorem continuous_within_at.norm {α : Type u_1} {E : Type u_3} {f : α → E} {s : set α} {a : α} (h : a) :
continuous_within_at (λ (x : α), f x) s a
theorem continuous_within_at.nnnorm {α : Type u_1} {E : Type u_3} {f : α → E} {s : set α} {a : α} (h : a) :
continuous_within_at (λ (x : α), f x∥₊) s a
theorem continuous_on.norm {α : Type u_1} {E : Type u_3} {f : α → E} {s : set α} (h : s) :
continuous_on (λ (x : α), f x) s
theorem continuous_on.nnnorm {α : Type u_1} {E : Type u_3} {f : α → E} {s : set α} (h : s) :
continuous_on (λ (x : α), f x∥₊) s
theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {E : Type u_3} {l : filter α} {f : α → E} (h : filter.tendsto (λ (y : α), f y) l filter.at_top) (x : E) :
∀ᶠ (y : α) in l, f y x

If ∥y∥→∞, then we can assume y≠x for any fixed x.

@[protected, instance]
def semi_normed_group.has_lipschitz_add {E : Type u_3}  :
@[protected, instance]
def normed_uniform_group {E : Type u_3}  :

A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

@[protected, instance]
def normed_top_group {E : Type u_3}  :
theorem nat.norm_cast_le {E : Type u_3} [has_one E] (n : ) :
theorem semi_normed_group.mem_closure_iff {E : Type u_3} {s : set E} {x : E} :
x ∀ (ε : ), ε > 0(∃ (y : E) (H : y s), x - y < ε)
theorem norm_le_zero_iff' {E : Type u_3} {g : E} :
g 0 g = 0
theorem norm_eq_zero_iff' {E : Type u_3} {g : E} :
g = 0 g = 0
theorem norm_pos_iff' {E : Type u_3} {g : E} :
0 < g g 0
theorem cauchy_seq_sum_of_eventually_eq {E : Type u_3} {u v : → E} {N : } (huv : ∀ (n : ), n Nu n = v n) (hv : cauchy_seq (λ (n : ), (finset.range (n + 1)).sum (λ (k : ), v k))) :
cauchy_seq (λ (n : ), (finset.range (n + 1)).sum (λ (k : ), u k))
def normed_group.of_add_dist {E : Type u_3} [has_norm E] [metric_space E] (H1 : ∀ (x : E), x = ) (H2 : ∀ (x y z : E), has_dist.dist (x + z) (y + z)) :

Construct a normed group from a translation invariant distance

Equations
structure normed_group.core (E : Type u_6) [has_norm E] :
Prop

A normed group can be built from a norm that satisfies algebraic properties. This is formalised in this structure.

The semi_normed_group.core induced by a normed_group.core.

def normed_group.of_core (E : Type u_1) [has_norm E] (C : normed_group.core E) :

Constructing a normed group from core properties of a norm, i.e., registering the distance and the metric space structure from the norm properties.

Equations
@[simp]
theorem norm_eq_zero {E : Type u_3} [normed_group E] {g : E} :
g = 0 g = 0
theorem norm_ne_zero_iff {E : Type u_3} [normed_group E] {g : E} :
g 0 g 0
@[simp]
theorem norm_pos_iff {E : Type u_3} [normed_group E] {g : E} :
0 < g g 0
@[simp]
theorem norm_le_zero_iff {E : Type u_3} [normed_group E] {g : E} :
g 0 g = 0
theorem norm_sub_eq_zero_iff {E : Type u_3} [normed_group E] {u v : E} :
u - v = 0 u = v
theorem eq_of_norm_sub_le_zero {E : Type u_3} [normed_group E] {g h : E} (a : g - h 0) :
g = h
theorem eq_of_norm_sub_eq_zero {E : Type u_3} [normed_group E] {u v : E} (h : u - v = 0) :
u = v
@[simp]
theorem nnnorm_eq_zero {E : Type u_3} [normed_group E] {a : E} :
a∥₊ = 0 a = 0
theorem nnnorm_ne_zero_iff {E : Type u_3} [normed_group E] {g : E} :
def normed_group.induced {F : Type u_4} [normed_group F] {E : Type u_1} (f : E →+ F) (h : function.injective f) :

An injective group homomorphism from an add_comm_group to a normed_group induces a normed_group structure on the domain.

Equations
@[protected, instance]
def add_subgroup.normed_group {E : Type u_3} [normed_group E] (s : add_subgroup E) :

A subgroup of a normed group is also a normed group, with the restriction of the norm.

Equations
@[protected, instance]
def submodule.normed_group {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [normed_group E] {_x_1 : E} (s : E) :

A submodule of a normed group is also a normed group, with the restriction of the norm.

Equations
@[protected, instance]
def ulift.normed_group {E : Type u_3} [normed_group E] :
Equations
@[protected, instance]
noncomputable def prod.normed_group {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] :

normed group instance on the product of two normed groups, using the sup norm.

Equations
@[protected, instance]
noncomputable def pi.normed_group {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group (π i)] :
normed_group (Π (i : ι), π i)

normed group instance on the product of finitely many normed groups, using the sup norm.

Equations
theorem tendsto_norm_sub_self_punctured_nhds {E : Type u_3} [normed_group E] (a : E) :
filter.tendsto (λ (x : E), x - a) {a}) (set.Ioi 0))
theorem tendsto_norm_nhds_within_zero {E : Type u_3} [normed_group E] :
(set.Ioi 0))

Some relations with has_compact_support

theorem has_compact_support_norm_iff {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} :
has_compact_support (λ (x : α), f x)
theorem has_compact_support.norm {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} :
has_compact_support (λ (x : α), f x)

Alias of the reverse direction of has_compact_support_norm_iff.

theorem continuous.bounded_above_of_compact_support {α : Type u_1} {E : Type u_3} [normed_group E] {f : α → E} (hf : continuous f) (hsupp : has_compact_support f) :
∃ (C : ), ∀ (x : α), f x C