mathlib documentation

analysis.normed.group.basic

Normed (semi)groups #

In this file we define four classes:

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

Tags #

normed group

def semi_normed_group.of_add_dist {E : Type u_3} [has_norm E] [add_comm_group E] [pseudo_metric_space E] (H1 : ∀ (x : E), x = dist x 0) (H2 : ∀ (x y z : E), dist x y 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] [add_comm_group E] [pseudo_metric_space E] (H1 : ∀ (x : E), x = dist x 0) (H2 : ∀ (x y z : E), dist (x + z) (y + z) dist x y) :

Construct a seminormed group from a translation invariant pseudodistance

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

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

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
@[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} [semi_normed_group E] (g h : E) :
dist g h = g - h
theorem dist_eq_norm' {E : Type u_3} [semi_normed_group E] (g h : E) :
dist g h = h - g
@[simp]
theorem dist_zero_right {E : Type u_3} [semi_normed_group E] (g : E) :
@[simp]
theorem dist_zero_left {E : Type u_3} [semi_normed_group E] :
theorem norm_sub_rev {E : Type u_3} [semi_normed_group E] (g h : E) :
g - h = h - g
@[simp]
theorem norm_neg {E : Type u_3} [semi_normed_group E] (g : E) :
@[simp]
theorem dist_add_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
dist (g + h₁) (g + h₂) = dist h₁ h₂
@[simp]
theorem dist_add_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
dist (g₁ + h) (g₂ + h) = dist g₁ g₂
@[simp]
theorem dist_neg_neg {E : Type u_3} [semi_normed_group E] (g h : E) :
dist (-g) (-h) = dist g h
@[simp]
theorem dist_sub_left {E : Type u_3} [semi_normed_group E] (g h₁ h₂ : E) :
dist (g - h₁) (g - h₂) = dist h₁ h₂
@[simp]
theorem dist_sub_right {E : Type u_3} [semi_normed_group E] (g₁ g₂ h : E) :
dist (g₁ - h) (g₂ - h) = dist g₁ g₂
theorem norm_add_le {E : Type u_3} [semi_normed_group E] (g h : E) :

Triangle inequality for the norm.

theorem norm_add_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ : E} {n₁ n₂ : } (H₁ : g₁ n₁) (H₂ : g₂ n₂) :
g₁ + g₂ n₁ + n₂
theorem dist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
dist (g₁ + g₂) (h₁ + h₂) dist g₁ h₁ + dist g₂ h₂
theorem dist_add_add_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : } (H₁ : dist g₁ h₁ d₁) (H₂ : dist g₂ h₂ d₂) :
dist (g₁ + g₂) (h₁ + h₂) d₁ + d₂
theorem dist_sub_sub_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
dist (g₁ - g₂) (h₁ - h₂) dist g₁ h₁ + dist g₂ h₂
theorem dist_sub_sub_le_of_le {E : Type u_3} [semi_normed_group E] {g₁ g₂ h₁ h₂ : E} {d₁ d₂ : } (H₁ : dist g₁ h₁ d₁) (H₂ : dist g₂ h₂ d₂) :
dist (g₁ - g₂) (h₁ - h₂) d₁ + d₂
theorem abs_dist_sub_le_dist_add_add {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
|dist g₁ h₁ - dist g₂ h₂| dist (g₁ + g₂) (h₁ + h₂)
@[simp]
theorem norm_nonneg {E : Type u_3} [semi_normed_group E] (g : E) :
@[simp]
theorem norm_zero {E : Type u_3} [semi_normed_group E] :
theorem norm_of_subsingleton {E : Type u_3} [semi_normed_group E] [subsingleton E] (x : E) :
theorem norm_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f : ι → E) :
∑ (i : ι) in s, f i ∑ (i : ι) in s, f i
theorem norm_sum_le_of_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) {f : ι → E} {n : ι → } (h : ∀ (b : ι), b sf b n b) :
∑ (b : ι) in s, f b ∑ (b : ι) in s, n b
theorem dist_sum_sum_le_of_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) {f g : ι → E} {d : ι → } (h : ∀ (b : ι), b sdist (f b) (g b) d b) :
dist (∑ (b : ι) in s, f b) (∑ (b : ι) in s, g b) ∑ (b : ι) in s, d b
theorem dist_sum_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f g : ι → E) :
dist (∑ (b : ι) in s, f b) (∑ (b : ι) in s, g b) ∑ (b : ι) in s, dist (f b) (g b)
theorem norm_sub_le {E : Type u_3} [semi_normed_group E] (g h : E) :
theorem norm_sub_le_of_le {E : Type u_3} [semi_normed_group E] {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} [semi_normed_group E] (g h : E) :
theorem abs_norm_sub_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
theorem norm_sub_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
theorem dist_norm_norm_le {E : Type u_3} [semi_normed_group E] (g h : E) :
theorem norm_le_insert {E : Type u_3} [semi_normed_group E] (u v : E) :
theorem norm_le_insert' {E : Type u_3} [semi_normed_group E] (u v : E) :
theorem norm_le_add_norm_add {E : Type u_3} [semi_normed_group E] (u v : E) :
theorem ball_zero_eq {E : Type u_3} [semi_normed_group E] (ε : ) :
metric.ball 0 ε = {x : E | x < ε}
theorem mem_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
theorem add_mem_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
theorem mem_ball_iff_norm' {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
@[simp]
theorem mem_ball_zero_iff {E : Type u_3} [semi_normed_group E] {ε : } {x : E} :
theorem mem_closed_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
theorem add_mem_closed_ball_iff_norm {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
theorem mem_closed_ball_iff_norm' {E : Type u_3} [semi_normed_group E] {g h : E} {r : } :
theorem norm_le_of_mem_closed_ball {E : Type u_3} [semi_normed_group E] {g h : E} {r : } (H : h metric.closed_ball g r) :
theorem norm_le_norm_add_const_of_dist_le {E : Type u_3} [semi_normed_group E] {a b : E} {c : } (h : dist a b c) :
theorem norm_lt_of_mem_ball {E : Type u_3} [semi_normed_group E] {g h : E} {r : } (H : h metric.ball g r) :
theorem norm_lt_norm_add_const_of_dist_lt {E : Type u_3} [semi_normed_group E] {a b : E} {c : } (h : dist a b < c) :
theorem bounded_iff_forall_norm_le {E : Type u_3} [semi_normed_group E] {s : set E} :
metric.bounded s ∃ (C : ), ∀ (x : E), x sx C
theorem preimage_add_ball {E : Type u_3} [semi_normed_group E] (x y : E) (r : ) :
theorem preimage_add_closed_ball {E : Type u_3} [semi_normed_group E] (x y : E) (r : ) :
@[simp]
theorem mem_sphere_iff_norm {E : Type u_3} [semi_normed_group E] (v w : E) (r : ) :
@[simp]
theorem mem_sphere_zero_iff_norm {E : Type u_3} [semi_normed_group E] {w : E} {r : } :
@[simp]
theorem norm_eq_of_mem_sphere {E : Type u_3} [semi_normed_group E] {r : } (x : (metric.sphere 0 r)) :
theorem preimage_add_sphere {E : Type u_3} [semi_normed_group E] (x y : E) (r : ) :
theorem ne_zero_of_norm_pos {E : Type u_3} [semi_normed_group E] {g : E} :
0 < gg 0
theorem nonzero_of_mem_sphere {E : Type u_3} [semi_normed_group E] {r : } (hr : 0 < r) (x : (metric.sphere 0 r)) :
x 0
theorem nonzero_of_mem_unit_sphere {E : Type u_3} [semi_normed_group E] (x : (metric.sphere 0 1)) :
x 0
@[protected, instance]
def metric.sphere.has_neg {E : Type u_3} [semi_normed_group E] {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} [semi_normed_group E] {r : } (v : (metric.sphere 0 r)) :
@[protected]
def isometric.add_right {E : Type u_3} [semi_normed_group E] (x : E) :
E ≃ᵢ E

Addition y ↦ y + x as an isometry.

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

Addition y ↦ x + y as an isometry.

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

Negation x ↦ -x as an isometry.

Equations
@[simp]
@[simp]
@[simp]
theorem normed_group.tendsto_nhds_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {l : filter α} :
filter.tendsto f l (𝓝 0) ∀ (ε : ), ε > 0(∀ᶠ (x : α) in l, f x < ε)
theorem normed_group.tendsto_nhds_nhds {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {x : E} {y : F} :
filter.tendsto f (𝓝 x) (𝓝 y) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x' : E), x' - x < δf x' - y < ε)
theorem normed_group.cauchy_seq_iff {α : Type u_1} {E : Type u_3} [semi_normed_group E] [nonempty α] [semilattice_sup α] {u : α → E} :
cauchy_seq u ∀ (ε : ), ε > 0(∃ (N : α), ∀ (m n : α), N mN nu m - u n < ε)
theorem add_monoid_hom.lipschitz_of_bound {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (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} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} {s : set E} :
lipschitz_on_with C f 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} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} {s : set E} (h : lipschitz_on_with C f 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} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} {s : set E} (h : lipschitz_on_with C f 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} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} :
lipschitz_with C f ∀ (x y : E), f x - f y (C) * x - y
theorem lipschitz_with.norm_sub_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} :
lipschitz_with C f∀ (x y : E), f x - f y (C) * x - y

Alias of lipschitz_with_iff_norm_sub_le.

theorem lipschitz_with.norm_sub_le_of_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {f : E → F} {C : ℝ≥0} (h : lipschitz_with C 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} [semi_normed_group E] [semi_normed_group F] (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} [semi_normed_group E] [topological_space α] {s : set α} (hs : is_compact s) {f : α → E} (hf : continuous_on f s) :
∃ (C : ), ∀ (x : α), x sf x C
theorem add_monoid_hom.isometry_iff_norm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) :
isometry f ∀ (x : E), f x = x
theorem add_monoid_hom.isometry_of_norm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) (hf : ∀ (x : E), f x = x) :
theorem controlled_sum_of_mem_closure {E : Type u_3} [semi_normed_group E] {s : add_subgroup E} {g : E} (hg : g closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (v : → E), filter.tendsto (λ (n : ), ∑ (i : ) in finset.range (n + 1), v i) filter.at_top (𝓝 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} [semi_normed_group E] [semi_normed_group F] {j : E →+ F} {h : F} (Hh : h closure (j.range)) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (g : → E), filter.tendsto (λ (n : ), ∑ (i : ) in finset.range (n + 1), j (g i)) filter.at_top (𝓝 h) j (g 0) - h < b 0 ∀ (n : ), n > 0j (g n) < b n
@[class]
structure has_nnnorm (E : Type u_5) :
Type u_5

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

Instances
@[protected, instance]
Equations
@[simp, norm_cast]
theorem coe_nnnorm {E : Type u_3} [semi_normed_group E] (a : E) :
theorem nndist_eq_nnnorm {E : Type u_3} [semi_normed_group E] (a b : E) :
@[simp]
theorem nnnorm_zero {E : Type u_3} [semi_normed_group E] :
theorem nnnorm_add_le {E : Type u_3} [semi_normed_group E] (g h : E) :
@[simp]
theorem nnnorm_neg {E : Type u_3} [semi_normed_group E] (g : E) :
theorem edist_eq_coe_nnnorm_sub {E : Type u_3} [semi_normed_group E] (x y : E) :
theorem edist_eq_coe_nnnorm {E : Type u_3} [semi_normed_group E] (x : E) :
theorem mem_emetric_ball_zero_iff {E : Type u_3} [semi_normed_group E] {x : E} {r : ℝ≥0∞} :
theorem nndist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
nndist (g₁ + g₂) (h₁ + h₂) nndist g₁ h₁ + nndist g₂ h₂
theorem edist_add_add_le {E : Type u_3} [semi_normed_group E] (g₁ g₂ h₁ h₂ : E) :
edist (g₁ + g₂) (h₁ + h₂) edist g₁ h₁ + edist g₂ h₂
theorem nnnorm_sum_le {ι : Type u_2} {E : Type u_3} [semi_normed_group E] (s : finset ι) (f : ι → E) :
∑ (a : ι) in s, f a∥₊ ∑ (a : ι) in s, f a∥₊
theorem add_monoid_hom.lipschitz_of_bound_nnnorm {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (f : E →+ F) (C : ℝ≥0) (h : ∀ (x : E), f x∥₊ C * x∥₊) :
theorem lipschitz_with.neg {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {K : ℝ≥0} {f : α → E} (hf : lipschitz_with K f) :
lipschitz_with K (λ (x : α), -f x)
theorem lipschitz_with.add {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : ℝ≥0} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x + g x)
theorem lipschitz_with.sub {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : ℝ≥0} {f g : α → E} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (λ (x : α), f x - g x)
theorem antilipschitz_with.add_lipschitz_with {α : Type u_1} {E : Type u_3} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : ℝ≥0} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg 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} [semi_normed_group E] [pseudo_emetric_space α] {Kf Kg : ℝ≥0} {f g : α → E} (hf : antilipschitz_with Kf f) (hg : lipschitz_with Kg (g - f)) (hK : Kg < Kf⁻¹) :
@[protected, instance]

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

Equations
@[simp]
theorem coe_norm_subgroup {E : Type u_1} [semi_normed_group E] {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.

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

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

See note [implicit instance arguments].

Equations
@[simp, norm_cast]
theorem submodule.norm_coe {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [semi_normed_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 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.

See note [implicit instance arguments].

@[simp]
theorem submodule.norm_mk {𝕜 : Type u_1} {_x : ring 𝕜} {E : Type u_2} [semi_normed_group E] {_x_1 : module 𝕜 E} {s : submodule 𝕜 E} (x : E) (hx : x s) :
x, hx⟩ = x
@[protected, instance]
noncomputable def prod.semi_normed_group {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] :

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

Equations
theorem prod.semi_norm_def {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
theorem prod.nnsemi_norm_def {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
theorem semi_norm_fst_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
theorem semi_norm_snd_le {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] (x : E × F) :
theorem semi_norm_prod_le_iff {E : Type u_3} {F : Type u_4} [semi_normed_group E] [semi_normed_group F] {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_semi_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_semi_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 semi_norm_le_pi_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :
@[simp]
theorem pi_semi_norm_const {ι : Type u_2} {E : Type u_3} [semi_normed_group E] [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnsemi_norm_const {ι : Type u_2} {E : Type u_3} [semi_normed_group E] [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a)∥₊ = a∥₊
theorem tendsto_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {a : filter α} {b : E} :
filter.tendsto f a (𝓝 b) filter.tendsto (λ (e : α), f e - b) a (𝓝 0)
theorem is_bounded_under_of_tendsto {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} {c : E} (h : filter.tendsto f l (𝓝 c)) :
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {a : filter α} :
filter.tendsto f a (𝓝 0) filter.tendsto (λ (e : α), f e) a (𝓝 0)
theorem squeeze_zero_norm' {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {g : α → } {t₀ : filter α} (h : ∀ᶠ (n : α) in t₀, f n g n) (h' : filter.tendsto g t₀ (𝓝 0)) :
filter.tendsto f t₀ (𝓝 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.ordered, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

theorem squeeze_zero_norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {f : α → E} {g : α → } {t₀ : filter α} (h : ∀ (n : α), f n g n) (h' : filter.tendsto g t₀ (𝓝 0)) :
filter.tendsto f t₀ (𝓝 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} [semi_normed_group E] (x : E) :
filter.tendsto (λ (g : E), g - x) (𝓝 x) (𝓝 0)
theorem tendsto_norm {E : Type u_3} [semi_normed_group E] {x : E} :
filter.tendsto (λ (g : E), g) (𝓝 x) (𝓝 x)
theorem tendsto_norm_zero {E : Type u_3} [semi_normed_group E] :
filter.tendsto (λ (g : E), g) (𝓝 0) (𝓝 0)
@[continuity]
theorem continuous_norm {E : Type u_3} [semi_normed_group E] :
continuous (λ (g : E), g)
@[continuity]
theorem continuous_nnnorm {E : Type u_3} [semi_normed_group E] :
continuous (λ (a : E), a∥₊)
theorem uniform_continuous_nnnorm {E : Type u_3} [semi_normed_group E] :
theorem filter.tendsto.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} {a : E} (h : filter.tendsto f l (𝓝 a)) :
filter.tendsto (λ (x : α), f x) l (𝓝 a)
theorem filter.tendsto.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] {l : filter α} {f : α → E} {a : E} (h : filter.tendsto f l (𝓝 a)) :
filter.tendsto (λ (x : α), f x∥₊) l (𝓝 a∥₊)
theorem continuous.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} (h : continuous f) :
continuous (λ (x : α), f x)
theorem continuous.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} (h : continuous f) :
continuous (λ (x : α), f x∥₊)
theorem continuous_at.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), f x) a
theorem continuous_at.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {a : α} (h : continuous_at f a) :
continuous_at (λ (x : α), f x∥₊) a
theorem continuous_within_at.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), f x) s a
theorem continuous_within_at.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), f x∥₊) s a
theorem continuous_on.norm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), f x) s
theorem continuous_on.nnnorm {α : Type u_1} {E : Type u_3} [semi_normed_group E] [topological_space α] {f : α → E} {s : set α} (h : continuous_on f s) :
continuous_on (λ (x : α), f x∥₊) s
theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {E : Type u_3} [semi_normed_group E] {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]
@[protected, instance]

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

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

Construct a normed group from a translation invariant distance

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

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

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
@[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
@[protected, instance]

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 : module 𝕜 E} (s : submodule 𝕜 E) :

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

See note [implicit instance arguments].

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
theorem prod.norm_def {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] (x : E × F) :
theorem prod.nnnorm_def {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] (x : E × F) :
theorem norm_fst_le {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] (x : E × F) :
theorem norm_snd_le {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] (x : E × F) :
theorem norm_prod_le_iff {E : Type u_3} {F : Type u_4} [normed_group E] [normed_group F] {x : E × F} {r : } :
@[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 pi_norm_le_iff {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] {r : } (hr : 0 r) {x : Π (i : ι), «π» i} :
x r ∀ (i : ι), x i r

The norm 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_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] {r : } (hr : 0 < r) {x : Π (i : ι), «π» i} :
x < r ∀ (i : ι), x i < r

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

theorem norm_le_pi_norm {ι : Type u_2} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :
@[simp]
theorem pi_norm_const {ι : Type u_2} {E : Type u_3} [normed_group E] [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnnorm_const {ι : Type u_2} {E : Type u_3} [normed_group E] [nonempty ι] [fintype ι] (a : E) :
(λ (i : ι), a)∥₊ = a∥₊