# mathlibdocumentation

analysis.normed_space.basic

# Normed spaces #

In this file we define (semi)normed spaces and algebras. We also prove some theorems about these definitions.

@[class]
structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α]  :
Type (max u_5 u_6)

A normed space over a normed field is a vector space endowed with a norm 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.

Note that since this requires seminormed_add_comm_group and not normed_add_comm_group, this typeclass can be used for "semi normed spaces" too, just as module can be used for "semi modules".

Instances of this typeclass
Instances of other typeclasses for normed_space
• normed_space.has_sizeof_inst
@[protected, instance]
def normed_space.has_bounded_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] :
@[protected, instance]
def normed_field.to_normed_space {α : Type u_1} [normed_field α] :
α
Equations
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] (s : α) (x : β) :
theorem norm_zsmul {β : Type u_2} (α : Type u_1) [normed_field α] [ β] (n : ) (x : β) :
@[simp]
theorem abs_norm_eq_norm {β : Type u_2} (z : β) :
theorem inv_norm_smul_mem_closed_unit_ball {β : Type u_2} [ β] (x : β) :
theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] (s : α) (x y : β) :
has_dist.dist (s x) (s y) = s *
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] (s : α) (x : β) :
theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] (s : α) (x y : β) :
has_nndist.nndist (s x) (s y) =
theorem lipschitz_with_smul {α : Type u_1} {β : Type u_2} [normed_field α] [ β] (s : α) :
theorem norm_smul_of_nonneg {β : Type u_2} [ β] {t : } (ht : 0 t) (x : β) :
theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [ E] (c : α) (x : E) {ε : } (h : 0 < ε) :
∀ᶠ (y : E) in nhds x, c (y - x) < ε
theorem filter.tendsto.zero_smul_is_bounded_under_le {α : Type u_1} {ι : Type u_4} [normed_field α] {E : Type u_5} [ E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : (nhds 0)) (hg : ) :
filter.tendsto (λ (x : ι), f x g x) l (nhds 0)
theorem filter.is_bounded_under.smul_tendsto_zero {α : Type u_1} {ι : Type u_4} [normed_field α] {E : Type u_5} [ E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : ) (hg : (nhds 0)) :
filter.tendsto (λ (x : ι), f x g x) l (nhds 0)
theorem closure_ball {E : Type u_5} [ E] (x : E) {r : } (hr : r 0) :
theorem frontier_ball {E : Type u_5} [ E] (x : E) {r : } (hr : r 0) :
theorem interior_closed_ball {E : Type u_5} [ E] (x : E) {r : } (hr : r 0) :
= r
theorem frontier_closed_ball {E : Type u_5} [ E] (x : E) {r : } (hr : r 0) :
=
@[protected, instance]
def add_subgroup.zmultiples.discrete_topology {E : Type u_1} [ E] (e : E) :
theorem homeomorph_unit_ball_apply_coe {E : Type u_5} [ E] (x : E) :
noncomputable def homeomorph_unit_ball {E : Type u_5} [ E] :
E ≃ₜ 1)

A (semi) normed real vector space is homeomorphic to the unit ball in the same space. This homeomorphism sends x : E to (1 + ∥x∥²)^(- ½) • x.

In many cases the actual implementation is not important, so we don't mark the projection lemmas homeomorph_unit_ball_apply_coe and homeomorph_unit_ball_symm_apply as @[simp].

See also cont_diff_homeomorph_unit_ball and cont_diff_on_homeomorph_unit_ball_symm for smoothness properties that hold when E is an inner-product space.

Equations
theorem homeomorph_unit_ball_symm_apply {E : Type u_5} [ E] (y : 1)) :
@[simp]
theorem coe_homeomorph_unit_ball_apply_zero {E : Type u_5} [ E] :
@[protected, instance]
def ulift.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [ E] :
(ulift E)
Equations
@[protected, instance]
def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [ E] {F : Type u_6} [ F] :
(E × F)

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

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

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

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

A subspace of a normed 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} [ 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 with nonzero norm 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.

@[protected, instance]
def normed_space.to_module' {α : Type u_1} [normed_field α] {F : Type u_6} [ F] :
F

While this may appear identical to normed_space.to_module, it contains an implicit argument involving normed_add_comm_group.to_seminormed_add_comm_group that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this normed_space.to_module':

example
(𝕜 ι : Type*) (E : ι → Type*)
[normed_field 𝕜] [Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)] :
Π i, module 𝕜 (E i) := by apply_instance


This Zulip thread gives some more context.

Equations
theorem exists_norm_eq (E : Type u_5) [ E] [nontrivial E] {c : } (hc : 0 c) :
∃ (x : E), x = c
@[simp]
theorem range_norm (E : Type u_5) [ E] [nontrivial E] :
theorem nnnorm_surjective (E : Type u_5) [ E] [nontrivial E] :
@[simp]
theorem range_nnnorm (E : Type u_5) [ E] [nontrivial E] :
theorem interior_closed_ball' {E : Type u_5} [ E] [nontrivial E] (x : E) (r : ) :
= r
theorem frontier_closed_ball' {E : Type u_5} [ E] [nontrivial E] (x : E) (r : ) :
=
theorem rescale_to_shell {α : Type u_1} [normed_field α] {E : Type u_5} [ 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.

theorem normed_space.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [ E] [nontrivial E] (c : ) :
∃ (x : E), c < x

If E is a nontrivial normed space over a nontrivially normed field 𝕜, then E is unbounded: for any c : ℝ, there exists a vector x : E with norm strictly greater than c.

@[protected]
theorem normed_space.unbounded_univ (𝕜 : Type u_5) (E : Type u_6) [ E] [nontrivial E] :
@[protected]
theorem normed_space.noncompact_space (𝕜 : Type u_5) (E : Type u_6) [ E] [nontrivial E] :

A normed vector space over a nontrivially normed field is a noncompact space. This cannot be an instance because in order to apply it, Lean would have to search for normed_space 𝕜 E with unknown 𝕜. We register this as an instance in two cases: 𝕜 = E and 𝕜 = ℝ.

@[protected, instance]
def nontrivially_normed_field.noncompact_space (𝕜 : Type u_5)  :
@[protected, instance]
def real_normed_space.noncompact_space (E : Type u_6) [nontrivial E] [ E] :
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :
Type (max u_5 u_6)

A normed algebra 𝕜' over 𝕜 is normed module that is also an algebra.

See the implementation notes for algebra for a discussion about non-unital algebras. Following the strategy there, a non-unital normed algebra can be written as:

variables [normed_field 𝕜] [non_unital_semi_normed_ring 𝕜']
variables [normed_module 𝕜 𝕜'] [smul_comm_class 𝕜 𝕜' 𝕜'] [is_scalar_tower 𝕜 𝕜' 𝕜']

Instances of this typeclass
Instances of other typeclasses for normed_algebra
• normed_algebra.has_sizeof_inst
@[protected, instance]
def normed_algebra.to_normed_space {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] :
𝕜'
Equations
@[protected, instance]
def normed_algebra.to_normed_space' {𝕜 : Type u_5} [normed_field 𝕜] {𝕜' : Type u_1} [normed_ring 𝕜'] [ 𝕜'] :
𝕜'

While this may appear identical to normed_algebra.to_normed_space, it contains an implicit argument involving normed_ring.to_semi_normed_ring that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this normed_space.to_module':

example
(𝕜 ι : Type*) (E : ι → Type*)
[normed_field 𝕜] [Π i, normed_ring (E i)] [Π i, normed_algebra 𝕜 (E i)] :
Π i, module 𝕜 (E i) := by apply_instance


See normed_space.to_module' for a similar situation.

Equations
theorem norm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] (x : 𝕜) :
theorem nnnorm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] (x : 𝕜) :
@[simp]
theorem norm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :
𝕜') x = x
@[simp]
theorem nnnorm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :
theorem algebra_map_isometry (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] [norm_one_class 𝕜'] :
isometry 𝕜')

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

@[simp]
theorem algebra_map_clm_coe_apply (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] (ᾰ : 𝕜) :
𝕜') = 𝕜')
def algebra_map_clm (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] :
𝕜 →L[𝕜] 𝕜'

The inclusion of the base field in a normed algebra as a continuous linear map.

Equations
@[simp]
theorem algebra_map_clm_apply (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] (ᾰ : 𝕜) :
𝕜') = 𝕜')
theorem algebra_map_clm_coe (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] :
𝕜') = 𝕜')
theorem algebra_map_clm_to_linear_map (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] :
𝕜').to_linear_map =
@[protected, instance]
def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :
Equations
@[protected, instance]
def normed_algebra_rat {𝕜 : Type u_1} [char_zero 𝕜] [ 𝕜] :

Any normed characteristic-zero division ring that is a normed_algebra over the reals is also a normed algebra over the rationals.

Phrased another way, if 𝕜 is a normed algebra over the reals, then algebra_rat respects that norm.

Equations
@[protected, instance]
def punit.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] :
Equations
@[protected, instance]
def ulift.normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [ 𝕜'] :
(ulift 𝕜')
Equations
@[protected, instance]
def prod.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_1} {F : Type u_2} [ E] [ F] :
(E × F)

The product of two normed algebras is a normed algebra, with the sup norm.

Equations
@[protected, instance]
noncomputable def pi.normed_algebra {ι : Type u_4} (𝕜 : Type u_5) [normed_field 𝕜] {E : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_ring (E i)] [Π (i : ι), (E i)] :
(Π (i : ι), E i)

The product of finitely many normed algebras is a normed algebra, with the sup norm.

Equations
@[protected, instance]
def restrict_scalars.seminormed_add_comm_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3}  :
Equations
@[protected, instance]
def restrict_scalars.normed_add_comm_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_add_comm_group E] :
Equations
@[protected, instance]
def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [ 𝕜'] (E : Type u_7) [ E] :
𝕜' E)

If E is a normed space over 𝕜' and 𝕜 is a normed algebra over 𝕜', then restrict_scalars.module is additionally a normed_space.

Equations
def module.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [I : E] :
𝕜' E)

The action of the original normed_field on restrict_scalars 𝕜 𝕜' E. This is not an instance as it would be contrary to the purpose of restrict_scalars.

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

Warning: This declaration should be used judiciously. Please consider using is_scalar_tower and/or restrict_scalars 𝕜 𝕜' E instead.

This definition allows the restrict_scalars.normed_space instance to be put directly on E rather on restrict_scalars 𝕜 𝕜' E. This would be a very bad instance; both because 𝕜' cannot be inferred, and because it is likely to create instance diamonds.

Equations