mathlib documentation

analysis.normed_space.basic

Normed spaces #

Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0 we start setting up the theory of semi_normed_group and we specialize to normed_group at the end.

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

Construct a seminormed group from a translation invariant pseudodistance

Equations
structure semi_normed_group.core (α : Type u_5) [add_comm_group α] [has_norm α] :
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.

Equations
@[simp]
theorem punit.norm_eq_zero (r : punit) :
@[instance]
Equations
theorem real.norm_eq_abs (r : ) :
theorem dist_eq_norm {α : Type u_1} [semi_normed_group α] (g h : α) :
dist g h = g - h
theorem dist_eq_norm' {α : Type u_1} [semi_normed_group α] (g h : α) :
dist g h = h - g
@[simp]
theorem dist_zero_right {α : Type u_1} [semi_normed_group α] (g : α) :
@[simp]
theorem dist_zero_left {α : Type u_1} [semi_normed_group α] :
theorem norm_sub_rev {α : Type u_1} [semi_normed_group α] (g h : α) :
g - h = h - g
@[simp]
theorem norm_neg {α : Type u_1} [semi_normed_group α] (g : α) :
@[simp]
theorem dist_add_left {α : Type u_1} [semi_normed_group α] (g h₁ h₂ : α) :
dist (g + h₁) (g + h₂) = dist h₁ h₂
@[simp]
theorem dist_add_right {α : Type u_1} [semi_normed_group α] (g₁ g₂ h : α) :
dist (g₁ + h) (g₂ + h) = dist g₁ g₂
@[simp]
theorem dist_neg_neg {α : Type u_1} [semi_normed_group α] (g h : α) :
dist (-g) (-h) = dist g h
@[simp]
theorem dist_sub_left {α : Type u_1} [semi_normed_group α] (g h₁ h₂ : α) :
dist (g - h₁) (g - h₂) = dist h₁ h₂
@[simp]
theorem dist_sub_right {α : Type u_1} [semi_normed_group α] (g₁ g₂ h : α) :
dist (g₁ - h) (g₂ - h) = dist g₁ g₂
theorem norm_add_le {α : Type u_1} [semi_normed_group α] (g h : α) :

Triangle inequality for the norm.

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

Addition y ↦ y + x as an isometry.

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

Addition y ↦ x + y as an isometry.

Equations
@[simp]
@[simp]
theorem isometric.coe_add_left {α : Type u_1} [semi_normed_group α] (x : α) :
@[simp]
theorem isometric.add_left_symm {α : Type u_1} [semi_normed_group α] (x : α) :
def isometric.neg (α : Type u_1) [semi_normed_group α] :
α ≃ᵢ α

Negation x ↦ -x as an isometry.

Equations
@[simp]
theorem isometric.neg_symm {α : Type u_1} [semi_normed_group α] :
@[simp]
theorem isometric.neg_to_equiv {α : Type u_1} [semi_normed_group α] :
@[simp]
theorem isometric.coe_neg {α : Type u_1} [semi_normed_group α] :
theorem normed_group.tendsto_nhds_zero {α : Type u_1} {γ : Type u_3} [semi_normed_group α] {f : γ → α} {l : filter γ} :
filter.tendsto f l (𝓝 0) ∀ (ε : ), ε > 0(∀ᶠ (x : γ) in l, f x < ε)
theorem normed_group.tendsto_nhds_nhds {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {f : α → β} {x : α} {y : β} :
filter.tendsto f (𝓝 x) (𝓝 y) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x' : α), x' - x < δf x' - y < ε)
theorem normed_group.cauchy_seq_iff {α : Type u_1} [semi_normed_group α] {u : → α} :
cauchy_seq u ∀ (ε : ), ε > 0(∃ (N : ), ∀ (m n : ), N mN nu m - u n < ε)
theorem cauchy_seq.add {α : Type u_1} [semi_normed_group α] {u v : → α} (hu : cauchy_seq u) (hv : cauchy_seq v) :
theorem cauchy_seq_sum_of_eventually_eq {α : Type u_1} [semi_normed_group α] {u v : → α} {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)
theorem add_monoid_hom.lipschitz_of_bound {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (f : α →+ β) (C : ) (h : ∀ (x : α), 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 {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} :
lipschitz_on_with C f s ∀ (x : α), x s∀ (y : α), y sf x - f y (C) * x - y
theorem lipschitz_on_with.norm_sub_le {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {f : α → β} {C : ℝ≥0} {s : set α} (h : lipschitz_on_with C f s) {x y : α} (x_in : x s) (y_in : y s) :
f x - f y (C) * x - y
theorem lipschitz_with_iff_norm_sub_le {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {f : α → β} {C : ℝ≥0} :
lipschitz_with C f ∀ (x y : α), f x - f y (C) * x - y
theorem add_monoid_hom.continuous_of_bound {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (f : α →+ β) (C : ) (h : ∀ (x : α), 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} [semi_normed_group α] {γ : Type u_2} [topological_space γ] {s : set γ} (hs : is_compact s) {f : γ → α} (hf : continuous_on f s) :
∃ (C : ), ∀ (x : γ), x sf x C
theorem add_monoid_hom.isometry_iff_norm {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (f : α →+ β) :
isometry f ∀ (x : α), f x = x
theorem add_monoid_hom.isometry_of_norm {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (f : α →+ β) (hf : ∀ (x : α), f x = x) :
theorem controlled_sum_of_mem_closure {α : Type u_1} [semi_normed_group α] {s : add_subgroup α} {g : α} (hg : g closure s) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (v : → α), 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 {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {j : α →+ β} {h : β} (Hh : h closure (j.range)) {b : } (b_pos : ∀ (n : ), 0 < b n) :
∃ (g : → α), 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 (α : Type u_5) :
Type u_5

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

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

@[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]
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
@[instance]
def prod.semi_normed_group {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] :

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

Equations
theorem prod.semi_norm_def {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (x : α × β) :
theorem prod.nnsemi_norm_def {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (x : α × β) :
theorem semi_norm_fst_le {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (x : α × β) :
theorem semi_norm_snd_le {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] (x : α × β) :
theorem semi_norm_prod_le_iff {α : Type u_1} {β : Type u_2} [semi_normed_group α] [semi_normed_group β] {x : α × β} {r : } :
@[instance]
def pi.semi_normed_group {ι : Type u_4} {π : ι → 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_4} {π : ι → 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_4} {π : ι → 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_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :
@[simp]
theorem pi_semi_norm_const {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [nonempty ι] [fintype ι] (a : α) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnsemi_norm_const {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [nonempty ι] [fintype ι] (a : α) :
(λ (i : ι), a)∥₊ = a∥₊
theorem tendsto_iff_norm_tendsto_zero {β : Type u_2} {ι : Type u_4} [semi_normed_group β] {f : ι → β} {a : filter ι} {b : β} :
filter.tendsto f a (𝓝 b) filter.tendsto (λ (e : ι), f e - b) a (𝓝 0)
theorem is_bounded_under_of_tendsto {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {l : filter ι} {f : ι → α} {c : α} (h : filter.tendsto f l (𝓝 c)) :
theorem tendsto_zero_iff_norm_tendsto_zero {β : Type u_2} {γ : Type u_3} [semi_normed_group β] {f : γ → β} {a : filter γ} :
filter.tendsto f a (𝓝 0) filter.tendsto (λ (e : γ), f e) a (𝓝 0)
theorem squeeze_zero_norm' {α : Type u_1} {γ : Type u_3} [semi_normed_group α] {f : γ → α} {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} {γ : Type u_3} [semi_normed_group α] {f : γ → α} {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 {α : Type u_1} [semi_normed_group α] (x : α) :
filter.tendsto (λ (g : α), g - x) (𝓝 x) (𝓝 0)
theorem tendsto_norm {α : Type u_1} [semi_normed_group α] {x : α} :
filter.tendsto (λ (g : α), g) (𝓝 x) (𝓝 x)
theorem tendsto_norm_zero {α : Type u_1} [semi_normed_group α] :
filter.tendsto (λ (g : α), g) (𝓝 0) (𝓝 0)
theorem continuous_norm {α : Type u_1} [semi_normed_group α] :
continuous (λ (g : α), g)
theorem continuous_nnnorm {α : Type u_1} [semi_normed_group α] :
continuous (λ (a : α), a∥₊)
theorem uniform_continuous_nnnorm {α : Type u_1} [semi_normed_group α] :
theorem filter.tendsto.norm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] {l : filter γ} {f : γ → α} {a : α} (h : filter.tendsto f l (𝓝 a)) :
filter.tendsto (λ (x : γ), f x) l (𝓝 a)
theorem filter.tendsto.nnnorm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] {l : filter γ} {f : γ → α} {a : α} (h : filter.tendsto f l (𝓝 a)) :
filter.tendsto (λ (x : γ), f x∥₊) l (𝓝 a∥₊)
theorem continuous.norm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} (h : continuous f) :
continuous (λ (x : γ), f x)
theorem continuous.nnnorm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} (h : continuous f) :
continuous (λ (x : γ), f x∥₊)
theorem continuous_at.norm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {a : γ} (h : continuous_at f a) :
continuous_at (λ (x : γ), f x) a
theorem continuous_at.nnnorm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {a : γ} (h : continuous_at f a) :
continuous_at (λ (x : γ), f x∥₊) a
theorem continuous_within_at.norm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {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} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {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} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {s : set γ} (h : continuous_on f s) :
continuous_on (λ (x : γ), f x) s
theorem continuous_on.nnnorm {α : Type u_1} {γ : Type u_3} [semi_normed_group α] [topological_space γ] {f : γ → α} {s : set γ} (h : continuous_on f s) :
continuous_on (λ (x : γ), f x∥₊) s
theorem eventually_ne_of_tendsto_norm_at_top {α : Type u_1} {γ : Type u_3} [semi_normed_group α] {l : filter γ} {f : γ → α} (h : filter.tendsto (λ (y : γ), f y) l filter.at_top) (x : α) :
∀ᶠ (y : γ) in l, f y x

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

@[instance]

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

@[instance]
def normed_top_monoid {α : Type u_1} [semi_normed_group α] :
@[instance]
theorem nat.norm_cast_le {α : Type u_1} [semi_normed_group α] [has_one α] (n : ) :
theorem semi_normed_group.mem_closure_iff {α : Type u_1} [semi_normed_group α] {s : set α} {x : α} :
x closure s ∀ (ε : ), ε > 0(∃ (y : α) (H : y s), x - y < ε)
theorem norm_le_zero_iff' {α : Type u_1} [semi_normed_group α] [separated_space α] {g : α} :
g 0 g = 0
theorem norm_eq_zero_iff' {α : Type u_1} [semi_normed_group α] [separated_space α] {g : α} :
g = 0 g = 0
theorem norm_pos_iff' {α : Type u_1} [semi_normed_group α] [separated_space α] {g : α} :
0 < g g 0
def normed_group.of_add_dist {α : Type u_1} [has_norm α] [add_comm_group α] [metric_space α] (H1 : ∀ (x : α), x = dist x 0) (H2 : ∀ (x y z : α), dist x y dist (x + z) (y + z)) :

Construct a normed group from a translation invariant distance

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

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

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

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 {α : Type u_1} [normed_group α] {g : α} :
g = 0 g = 0
@[simp]
theorem norm_pos_iff {α : Type u_1} [normed_group α] {g : α} :
0 < g g 0
@[simp]
theorem norm_le_zero_iff {α : Type u_1} [normed_group α] {g : α} :
g 0 g = 0
theorem eq_of_norm_sub_le_zero {α : Type u_1} [normed_group α] {g h : α} (a : g - h 0) :
g = h
theorem eq_of_norm_sub_eq_zero {α : Type u_1} [normed_group α] {u v : α} (h : u - v = 0) :
u = v
theorem norm_sub_eq_zero_iff {α : Type u_1} [normed_group α] {u v : α} :
u - v = 0 u = v
@[simp]
theorem nnnorm_eq_zero {α : Type u_1} [normed_group α] {a : α} :
a∥₊ = 0 a = 0
@[instance]

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

Equations
@[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
@[instance]
def prod.normed_group {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] :

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

Equations
theorem prod.norm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :
theorem prod.nnnorm_def {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :
theorem norm_fst_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :
theorem norm_snd_le {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] (x : α × β) :
theorem norm_prod_le_iff {α : Type u_1} {β : Type u_2} [normed_group α] [normed_group β] {x : α × β} {r : } :
@[instance]
def pi.normed_group {ι : Type u_4} {π : ι → 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_4} {π : ι → 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_4} {π : ι → 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_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_group («π» i)] (x : Π (i : ι), «π» i) (i : ι) :
@[simp]
theorem pi_norm_const {α : Type u_1} {ι : Type u_4} [normed_group α] [nonempty ι] [fintype ι] (a : α) :
(λ (i : ι), a) = a
@[simp]
theorem pi_nnnorm_const {α : Type u_1} {ι : Type u_4} [normed_group α] [nonempty ι] [fintype ι] (a : α) :
(λ (i : ι), a)∥₊ = a∥₊
@[class]
structure semi_normed_ring (α : Type u_5) :
Type u_5

A seminormed ring is a ring endowed with a seminorm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[class]
structure normed_ring (α : Type u_5) :
Type u_5

A normed ring is a ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[class]
structure semi_normed_comm_ring (α : Type u_5) :
Type u_5

A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[class]
structure normed_comm_ring (α : Type u_5) :
Type u_5
  • to_normed_ring : normed_ring α
  • mul_comm : ∀ (x y : α), x * y = y * x

A normed commutative ring is a commutative ring endowed with a norm which satisfies the inequality ∥x y∥ ≤ ∥x∥ ∥y∥.

Instances
@[instance]
Equations
@[class]
structure norm_one_class (α : Type u_5) [has_norm α] [has_one α] :
Prop

A mixin class with the axiom ∥1∥ = 1. Many normed_rings and all normed_fields satisfy this axiom.

Instances
@[simp]
theorem nnnorm_one {α : Type u_1} [semi_normed_group α] [has_one α] [norm_one_class α] :
@[instance]
def prod.norm_one_class {α : Type u_1} {β : Type u_2} [normed_group α] [has_one α] [norm_one_class α] [normed_group β] [has_one β] [norm_one_class β] :
theorem norm_mul_le {α : Type u_1} [semi_normed_ring α] (a b : α) :
@[instance]
def subalgebra.semi_normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} [semi_normed_ring E] {_x_1 : algebra 𝕜 E} (s : subalgebra 𝕜 E) :

A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.

See note [implicit instance arguments].

Equations
@[instance]
def subalgebra.normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} [normed_ring E] {_x_1 : algebra 𝕜 E} (s : subalgebra 𝕜 E) :

A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.

See note [implicit instance arguments].

Equations
theorem list.norm_prod_le' {α : Type u_1} [semi_normed_ring α] {l : list α} :
theorem list.norm_prod_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (l : list α) :
theorem finset.norm_prod_le' {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] (s : finset ι) (hs : s.nonempty) (f : ι → α) :
∏ (i : ι) in s, f i ∏ (i : ι) in s, f i
theorem finset.norm_prod_le {ι : Type u_4} {α : Type u_1} [normed_comm_ring α] [norm_one_class α] (s : finset ι) (f : ι → α) :
∏ (i : ι) in s, f i ∏ (i : ι) in s, f i
theorem norm_pow_le' {α : Type u_1} [semi_normed_ring α] (a : α) {n : } :
0 < na ^ n a ^ n

If α is a seminormed ring, then ∥a^n∥≤ ∥a∥^n for n > 0. See also norm_pow_le.

theorem norm_pow_le {α : Type u_1} [semi_normed_ring α] [norm_one_class α] (a : α) (n : ) :

If α is a seminormed ring with ∥1∥=1, then ∥a^n∥≤ ∥a∥^n. See also norm_pow_le'.

theorem eventually_norm_pow_le {α : Type u_1} [semi_normed_ring α] (a : α) :
∀ᶠ (n : ) in filter.at_top, a ^ n a ^ n
theorem mul_left_bound {α : Type u_1} [semi_normed_ring α] (x y : α) :

In a seminormed ring, the left-multiplication add_monoid_hom is bounded.

theorem mul_right_bound {α : Type u_1} [semi_normed_ring α] (x y : α) :

In a seminormed ring, the right-multiplication add_monoid_hom is bounded.

@[instance]
def prod.semi_normed_ring {α : Type u_1} {β : Type u_2} [semi_normed_ring α] [semi_normed_ring β] :

Seminormed ring structure on the product of two seminormed rings, using the sup norm.

Equations
theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : units α) :
@[instance]
def prod.normed_ring {α : Type u_1} {β : Type u_2} [normed_ring α] [normed_ring β] :
normed_ring × β)

Normed ring structure on the product of two normed rings, using the sup norm.

Equations
@[instance]
@[instance]
def semi_normed_top_ring {α : Type u_1} [semi_normed_ring α] :

A seminormed ring is a topological ring.

@[class]
structure normed_field (α : Type u_5) :
Type u_5

A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥.

Instances
@[class]
structure nondiscrete_normed_field (α : Type u_5) :
Type u_5

A nondiscrete normed field is a normed field in which there is an element of norm different from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by multiplication by the powers of any element, and thus to relate algebra and topology.

Instances
@[simp]
theorem normed_field.norm_mul {α : Type u_1} [normed_field α] (a b : α) :
@[instance]
@[simp]
theorem normed_field.nnnorm_mul {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.norm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
@[simp]
theorem normed_field.nnnorm_hom_apply {α : Type u_1} [normed_field α] (ᾰ : α) :
@[simp]
theorem normed_field.norm_pow {α : Type u_1} [normed_field α] (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem normed_field.nnnorm_pow {α : Type u_1} [normed_field α] (a : α) (n : ) :
@[simp]
theorem normed_field.norm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
∏ (b : β) in s, f b = ∏ (b : β) in s, f b
@[simp]
theorem normed_field.nnnorm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
∏ (b : β) in s, f b∥₊ = ∏ (b : β) in s, f b∥₊
@[simp]
theorem normed_field.norm_div {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.nnnorm_div {α : Type u_1} [normed_field α] (a b : α) :
@[simp]
theorem normed_field.norm_inv {α : Type u_1} [normed_field α] (a : α) :
@[simp]
theorem normed_field.nnnorm_inv {α : Type u_1} [normed_field α] (a : α) :
@[simp]
theorem normed_field.norm_fpow {α : Type u_1} [normed_field α] (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem normed_field.nnnorm_fpow {α : Type u_1} [normed_field α] (a : α) (n : ) :
theorem normed_field.exists_one_lt_norm (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 1 < x
theorem normed_field.exists_norm_lt_one (α : Type u_1) [nondiscrete_normed_field α] :
∃ (x : α), 0 < x x < 1
theorem normed_field.exists_lt_norm (α : Type u_1) [nondiscrete_normed_field α] (r : ) :
∃ (x : α), r < x
theorem normed_field.exists_norm_lt (α : Type u_1) [nondiscrete_normed_field α] {r : } (hr : 0 < r) :
∃ (x : α), 0 < x x < r
@[instance]
theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} [nondiscrete_normed_field α] (x : α) :
@[instance]
theorem real.norm_of_nonneg {x : } (hx : 0 x) :
theorem real.norm_of_nonpos {x : } (hx : x 0) :
@[simp]
theorem real.norm_coe_nat (n : ) :
@[simp]
@[simp]
theorem real.norm_two  :
@[simp]
theorem real.nnnorm_two  :
theorem real.nnnorm_of_nonneg {x : } (hx : 0 x) :
x∥₊ = x, hx⟩
@[simp]
theorem nnreal.norm_eq (x : ℝ≥0) :
@[simp]
theorem nnreal.nnnorm_eq (x : ℝ≥0) :
@[simp]
theorem norm_norm {α : Type u_1} [semi_normed_group α] (x : α) :
@[simp]
theorem nnnorm_norm {α : Type u_1} [semi_normed_group α] (a : α) :
theorem normed_group.tendsto_at_top {α : Type u_1} [nonempty α] [semilattice_sup α] {β : Type u_2} [semi_normed_group β] {f : α → β} {b : β} :
filter.tendsto f filter.at_top (𝓝 b) ∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N nf n - b < ε)

A restatement of metric_space.tendsto_at_top in terms of the norm.

theorem normed_group.tendsto_at_top' {α : Type u_1} [nonempty α] [semilattice_sup α] [no_top_order α] {β : Type u_2} [semi_normed_group β] {f : α → β} {b : β} :
filter.tendsto f filter.at_top (𝓝 b) ∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N < nf n - b < ε)

A variant of normed_group.tendsto_at_top that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

@[instance]
Equations
theorem int.norm_eq_abs (n : ) :
@[instance]
Equations
@[simp]
theorem rat.norm_cast_real (r : ) :
@[simp]
theorem int.norm_cast_rat (m : ) :
theorem norm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem norm_gsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem nnnorm_nsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
theorem nnnorm_gsmul_le {α : Type u_1} [semi_normed_group α] (n : ) (a : α) :
@[class]
structure semi_normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [semi_normed_group β] :
Type (max u_5 u_6)

A seminormed space over a normed field is a vector space endowed with a seminorm which satisfies the equality ∥c • x∥ = ∥c∥ ∥x∥. We require only ∥c • x∥ ≤ ∥c∥ ∥x∥ in the definition, then prove ∥c • x∥ = ∥c∥ ∥x∥ in norm_smul.

Instances
@[instance]
def normed_space.to_semi_normed_space {α : Type u_1} {β : Type u_2} [normed_field α] [normed_group β] [γ : normed_space α β] :

A normed space is a seminormed space.

Equations
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x : β) :
@[simp]
theorem abs_norm_eq_norm {β : Type u_2} [semi_normed_group β] (z : β) :
theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x y : β) :
dist (s x) (s y) = s * dist x y
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x : β) :
theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [semi_normed_space α β] (s : α) (x y : β) :
nndist (s x) (s y) = s∥₊ * nndist x y
theorem norm_smul_of_nonneg {β : Type u_2} [semi_normed_group β] [semi_normed_space β] {t : } (ht : 0 t) (x : β) :
@[instance]
theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] (c : α) (x : E) {ε : } (h : 0 < ε) :
∀ᶠ (y : E) in 𝓝 x, c (y - x) < ε
theorem closure_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem frontier_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem interior_closed_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem frontier_closed_ball {E : Type u_5} [semi_normed_group E] [semi_normed_space E] (x : E) {r : } (hr : 0 < r) :
theorem ne_neg_of_mem_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] [char_zero α] {r : } (hr : 0 < r) (x : (metric.sphere 0 r)) :
x -x
theorem ne_neg_of_mem_unit_sphere (α : Type u_1) [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] [char_zero α] (x : (metric.sphere 0 1)) :
x -x
@[instance]
def prod.semi_normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] {F : Type u_6} [semi_normed_group F] [semi_normed_space α F] :

The product of two seminormed spaces is a seminormed space, with the sup norm.

Equations
@[instance]
def pi.semi_normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), semi_normed_group (E i)] [Π (i : ι), semi_normed_space α (E i)] :
semi_normed_space α (Π (i : ι), E i)

The product of finitely many seminormed spaces is a seminormed space, with the sup norm.

Equations
@[instance]
def submodule.semi_normed_space {𝕜 : Type u_1} {R : Type u_2} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [semi_normed_group E] [semi_normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :

A subspace of a seminormed space is also a normed space, with the restriction of the norm.

Equations
theorem rescale_to_shell_semi_normed {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [semi_normed_space α E] {c : α} (hc : 1 < c) {ε : } (εpos : 0 < ε) {x : E} (hx : x 0) :
∃ (d : α), d 0 d x < ε ε / c d x d⁻¹ ⁻¹ * c) * x

If there is a scalar c with ∥c∥>1, then any element of with norm different from 0 can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.

theorem interior_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (r : ) :
theorem frontier_closed_ball' {E : Type u_5} [normed_group E] [normed_space E] [nontrivial E] (x : E) (r : ) :
theorem rescale_to_shell {α : Type u_1} [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] {c : α} (hc : 1 < c) {ε : } (εpos : 0 < ε) {x : E} (hx : x 0) :
∃ (d : α), d 0 d x < ε ε / c d x d⁻¹ ⁻¹ * c) * x

If there is a scalar c with ∥c∥>1, then any element can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.

@[instance]
def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [normed_group E] [normed_space α E] {F : Type u_6} [normed_group F] [normed_space α F] :
normed_space α (E × F)

The product of two normed spaces is a normed space, with the sup norm.

Equations
@[instance]
def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), normed_group (E i)] [Π (i : ι), normed_space α (E i)] :
normed_space α (Π (i : ι), E i)

The product of finitely many normed spaces is a normed space, with the sup norm.

Equations
@[instance]
def submodule.normed_space {𝕜 : Type u_1} {R : Type u_2} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :

A subspace of a normed space is also a normed space, with the restriction of the norm.

Equations
@[class]
structure semi_normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :
Type (max u_5 u_6)

A seminormed algebra 𝕜' over 𝕜 is an algebra endowed with a seminorm for which the embedding of 𝕜 in 𝕜' is an isometry.

Instances
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_ring 𝕜'] :
Type (max u_5 u_6)

A normed algebra 𝕜' over 𝕜 is an algebra endowed with a norm for which the embedding of 𝕜 in 𝕜' is an isometry.

Instances
@[instance]
def normed_algebra.to_semi_normed_algebra (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

A normed algebra is a seminormed algebra.

Equations
@[simp]
theorem norm_algebra_map_eq {𝕜 : Type u_1} (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [h : semi_normed_algebra 𝕜 𝕜'] (x : 𝕜) :
(algebra_map 𝕜 𝕜') x = x
theorem algebra_map_isometry (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :

In a normed algebra, the inclusion of the base field in the extended field is an isometry.

@[instance]
def normed_algebra.to_normed_space (𝕜 : Type u_1) [normed_field 𝕜] (𝕜' : Type u_2) [normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
theorem normed_algebra.norm_one (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
theorem normed_algebra.norm_one_class (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
theorem normed_algebra.zero_ne_one (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
0 1
theorem normed_algebra.nontrivial (𝕜 : Type u_5) [normed_field 𝕜] (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [semi_normed_algebra 𝕜 𝕜'] :
def semi_normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (F : Type u_8) [semi_normed_group F] [semi_normed_space 𝕜' F] :

Warning: This declaration should be used judiciously. Please consider using is_scalar_tower instead.

𝕜-seminormed space structure induced by a 𝕜'-seminormed space structure when 𝕜' is a seminormed algebra over 𝕜. Not registered as an instance as 𝕜' can not be inferred.

The type synonym module.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations
def normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group E] [normed_space 𝕜' E] :

Warning: This declaration should be used judiciously. Please consider using is_scalar_tower instead.

𝕜-normed space structure induced by a 𝕜'-normed space structure when 𝕜' is a normed algebra over 𝕜. Not registered as an instance as 𝕜' can not be inferred.

The type synonym module.restrict_scalars 𝕜 𝕜' E will be endowed with this instance by default.

Equations
@[instance]
def restrict_scalars.semi_normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {F : Type u_3} [I : semi_normed_group F] :
Equations
@[instance]
def restrict_scalars.normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_group E] :
Equations
@[instance]
def module.restrict_scalars.semi_normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {F : Type u_3} [normed_field 𝕜'] [semi_normed_group F] [I : semi_normed_space 𝕜' F] :
semi_normed_space 𝕜' (restrict_scalars 𝕜 𝕜' F)
Equations
@[instance]
def module.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [normed_group E] [I : normed_space 𝕜' E] :
normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E)
Equations
@[instance]
def restrict_scalars.semi_normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (F : Type u_8) [semi_normed_group F] [semi_normed_space 𝕜' F] :
Equations
@[instance]
def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [normed_group E] [normed_space 𝕜' E] :
normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E)
Equations
theorem cauchy_seq_finset_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i) ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)
theorem summable_iff_vanishing_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} :
summable f ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)
theorem cauchy_seq_finset_of_norm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (g : ι → ) (hg : summable g) (h : ∀ (i : ι), f i g i) :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)
theorem cauchy_seq_finset_of_summable_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (hf : summable (λ (a : ι), f a)) :
cauchy_seq (λ (s : finset ι), ∑ (a : ι) in s, f a)
theorem has_sum_of_subseq_of_summable {α : Type u_1} {γ : Type u_3} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (hf : summable (λ (a : ι), f a)) {s : γ → finset ι} {p : filter γ} [p.ne_bot] (hs : filter.tendsto s p filter.at_top) {a : α} (ha : filter.tendsto (λ (b : γ), ∑ (i : ι) in s b, f i) p (𝓝 a)) :

If a function f is summable in norm, and along some sequence of finsets exhausting the space its sum is converging to a limit a, then this holds along all finsets, i.e., f is summable with sum a.

theorem has_sum_iff_tendsto_nat_of_summable_norm {α : Type u_1} [semi_normed_group α] {f : → α} {a : α} (hf : summable (λ (i : ), f i)) :
has_sum f a filter.tendsto (λ (n : ), ∑ (i : ) in finset.range n, f i) filter.at_top (𝓝 a)
theorem summable_of_norm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (g : ι → ) (hg : summable g) (h : ∀ (i : ι), f i g i) :

The direct comparison test for series: if the norm of f is bounded by a real function g which is summable, then f is summable.

theorem has_sum.norm_le_of_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} {g : ι → } {a : α} {b : } (hf : has_sum f a) (hg : has_sum g b) (h : ∀ (i : ι), f i g i) :
theorem tsum_of_norm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} {g : ι → } {a : } (hg : has_sum g a) (h : ∀ (i : ι), f i g i) :
∑' (i : ι), f i a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ∥f i∥ ≤ g i, then ∥∑' i, f i∥ ≤ ∑' i, g i. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem norm_tsum_le_tsum_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (hf : summable (λ (i : ι), f i)) :
∑' (i : ι), f i ∑' (i : ι), f i

If ∑' i, ∥f i∥ is summable, then ∥∑' i, f i∥ ≤ (∑' i, ∥f i∥). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem tsum_of_nnnorm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : has_sum g a) (h : ∀ (i : ι), f i∥₊ g i) :
∑' (i : ι), f i∥₊ a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, nnnorm (f i) ≤ g i, then nnnorm (∑' i, f i) ≤ ∑' i, g i. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem nnnorm_tsum_le {α : Type u_1} {ι : Type u_4} [semi_normed_group α] {f : ι → α} (hf : summable (λ (i : ι), f i∥₊)) :
∑' (i : ι), f i∥₊ ∑' (i : ι), f i∥₊

If ∑' i, nnnorm (f i) is summable, then nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem summable_of_norm_bounded_eventually {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (g : ι → ) (hg : summable g) (h : ∀ᶠ (i : ι) in filter.cofinite, f i g i) :

Variant of the direct comparison test for series: if the norm of f is eventually bounded by a real function g which is summable, then f is summable.

theorem summable_of_nnnorm_bounded {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (g : ι → ℝ≥0) (hg : summable g) (h : ∀ (i : ι), f i∥₊ g i) :
theorem summable_of_summable_norm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), f a)) :
theorem summable_of_summable_nnnorm {α : Type u_1} {ι : Type u_4} [semi_normed_group α] [complete_space α] {f : ι → α} (hf : summable (λ (a : ι), f a∥₊)) :
@[simp]
theorem uniform_space.completion.norm_coe {V : Type u_1} [semi_normed_group V] (v : V) :