mathlib documentation

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 α] [seminormed_add_comm_group β] :
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 α] [seminormed_add_comm_group β] [normed_space α β] :
theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :
theorem norm_zsmul {β : Type u_2} [seminormed_add_comm_group β] (α : Type u_1) [normed_field α] [normed_space α β] (n : ) (x : β) :
@[simp]
theorem abs_norm_eq_norm {β : Type u_2} [seminormed_add_comm_group β] (z : β) :
theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x y : β) :
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :
theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x y : β) :
theorem lipschitz_with_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) :
theorem norm_smul_of_nonneg {β : Type u_2} [seminormed_add_comm_group β] [normed_space β] {t : } (ht : 0 t) (x : β) :
theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α 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} [seminormed_add_comm_group E] [normed_space α E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm g)) :
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} [seminormed_add_comm_group E] [normed_space α E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : filter.is_bounded_under has_le.le l (has_norm.norm f)) (hg : filter.tendsto g l (nhds 0)) :
filter.tendsto (λ (x : ι), f x g x) l (nhds 0)
theorem closure_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space E] (x : E) {r : } (hr : r 0) :
theorem frontier_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space E] (x : E) {r : } (hr : r 0) :
theorem interior_closed_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space E] (x : E) {r : } (hr : r 0) :
theorem frontier_closed_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space E] (x : E) {r : } (hr : r 0) :
noncomputable def homeomorph_unit_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space E] :

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
@[protected, instance]
def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] {F : Type u_6} [seminormed_add_comm_group F] [normed_space α F] :
normed_space α (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 : ι), seminormed_add_comm_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
@[protected, instance]
def submodule.normed_space {𝕜 : Type u_1} {R : Type u_2} [has_smul 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [seminormed_add_comm_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
theorem rescale_to_shell_semi_normed {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_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 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} [normed_add_comm_group F] [normed_space α F] :
module α 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) [normed_add_comm_group E] [normed_space E] [nontrivial E] {c : } (hc : 0 c) :
∃ (x : E), x = c
theorem rescale_to_shell {α : Type u_1} [normed_field α] {E : Type u_5} [normed_add_comm_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.

theorem normed_space.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 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]
@[protected]
theorem normed_space.noncompact_space (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 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]
@[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 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
@[protected, instance]
def normed_algebra.to_normed_space' {𝕜 : Type u_5} [normed_field 𝕜] {𝕜' : Type u_1} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'

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 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :
theorem nnnorm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :
@[simp]
theorem norm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :
(algebra_map 𝕜 𝕜') x = x
@[simp]
theorem nnnorm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :
@[simp]
theorem norm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra 𝕜'] (x : nnreal) :
@[simp]
theorem nnnorm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra 𝕜'] (x : nnreal) :
theorem algebra_map_isometry (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] :

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

@[protected, instance]
def normed_algebra_rat {𝕜 : Type u_1} [normed_division_ring 𝕜] [char_zero 𝕜] [normed_algebra 𝕜] :

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 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_algebra 𝕜 (ulift 𝕜')
Equations
@[protected, instance]
def prod.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_1} {F : Type u_2} [semi_normed_ring E] [semi_normed_ring F] [normed_algebra 𝕜 E] [normed_algebra 𝕜 F] :
normed_algebra 𝕜 (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 : ι), normed_algebra 𝕜 (E i)] :
normed_algebra 𝕜 (Π (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} [I : seminormed_add_comm_group E] :
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 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [seminormed_add_comm_group E] [normed_space 𝕜' E] :
normed_space 𝕜 (restrict_scalars 𝕜 𝕜' 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 𝕜'] [seminormed_add_comm_group E] [I : normed_space 𝕜' E] :
normed_space 𝕜' (restrict_scalars 𝕜 𝕜' 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 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [seminormed_add_comm_group E] [normed_space 𝕜' 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