# mathlib3documentation

analysis.normed_space.basic

# Normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 real.module  :
Equations
@[protected, instance]
def normed_field.to_normed_space {α : Type u_1} [normed_field α] :
α
Equations
@[protected, instance]
theorem norm_zsmul {β : Type u_2} (α : Type u_1) [normed_field α] [ β] (n : ) (x : β) :
@[simp]
theorem abs_norm {β : Type u_2} (z : β) :
theorem inv_norm_smul_mem_closed_unit_ball {β : Type u_2} [ β] (x : β) :
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) :
=
theorem interior_sphere {E : Type u_5} [ E] (x : E) {r : } (hr : r 0) :
theorem frontier_sphere {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) :
= ( (1 + x ^ 2))⁻¹ x
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 mul_opposite.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [ E] :
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_zpow {α : Type u_1} [normed_field α] {E : Type u_5} [ E] {c : α} (hc : 1 < c) {ε : } (εpos : 0 < ε) {x : E} (hx : x 0) :
(n : ), c ^ n 0 c ^ n x < ε ε / c c ^ n x c ^ n⁻¹ ε⁻¹ * 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.

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) :

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.

@[reducible]
def normed_space.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [ β] [ γ] [ β γ] (f : F) :
β

A linear map from a module to a normed_space induces a normed_space structure on the domain, using the seminormed_add_comm_group.induced norm.

Equations
@[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] :
@[protected, instance]
def real.punctured_nhds_module_ne_bot {E : Type u_1} [nontrivial E] [ E] (x : E) :
{x}).ne_bot

If E is a nontrivial topological module over ℝ, then E has no isolated points. This is a particular case of module.punctured_nhds_ne_bot.

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 : ) :
=
@[simp]
theorem interior_sphere' {E : Type u_5} [ E] [nontrivial E] (x : E) (r : ) :
@[simp]
theorem frontier_sphere' {E : Type u_5} [ E] [nontrivial E] (x : E) (r : ) :
theorem rescale_to_shell_zpow {α : Type u_1} [normed_field α] {E : Type u_5} [ E] {c : α} (hc : 1 < c) {ε : } (εpos : 0 < ε) {x : E} (hx : x 0) :
(n : ), c ^ n 0 c ^ n x < ε ε / c c ^ n x c ^ n⁻¹ ε⁻¹ * c * x
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) :

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]
@[protected, instance]
@[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 : 𝕜) :
@[simp]
theorem norm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [ 𝕜'] (x : nnreal) :
𝕜') x = x
@[simp]
theorem nnnorm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [ 𝕜'] (x : nnreal) :
𝕜') x‖₊ = 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.

@[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]
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 mul_opposite.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_1} [ E] :
Equations
@[reducible]
def normed_algebra.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [ring β] [ β] [ γ] [ γ] (f : F) :

A non-unital algebra homomorphism from an algebra to a normed_algebra induces a normed_algebra structure on the domain, using the semi_normed_ring.induced norm.

Equations
@[protected, instance]
def subalgebra.to_normed_algebra {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [ A] (S : A) :
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