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 α] [semi_normed_group β] :

Type (max u_5 u_6)

to_module : module α β
norm_smul_le : ∀ (a : α) (b : β), ∥a • b∥ ≤ ∥a∥ * ∥b∥

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 semi_normed_group and not normed_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 α] [semi_normed_group β] [normed_space α β] :

has_bounded_smul α β

@[protected, instance]

def normed_field.to_normed_space {α : Type u_1} [normed_field α] :

normed_space α α

Equations

normed_field.to_normed_space = {to_module := semiring.to_module ring.to_semiring, norm_smul_le := _}

theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x : β) :

∥s • x∥ = ∥s∥ * ∥x∥

@[simp]

theorem abs_norm_eq_norm {β : Type u_2} [semi_normed_group β] (z : β) :

|∥z∥| = ∥z∥

theorem inv_norm_smul_mem_closed_unit_ball {β : Type u_2} [semi_normed_group β] [normed_space ℝ β] (x : β) :

∥x∥⁻¹ • x ∈ metric.closed_ball 0 1

theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x y : β) :

has_dist.dist (s • x) (s • y) = ∥s∥ * has_dist.dist x y

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x : β) :

∥s • x∥₊ = ∥s∥₊ * ∥x∥₊

theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) (x y : β) :

has_nndist.nndist (s • x) (s • y) = ∥s∥₊ * has_nndist.nndist x y

theorem lipschitz_with_smul {α : Type u_1} {β : Type u_2} [normed_field α] [semi_normed_group β] [normed_space α β] (s : α) :

lipschitz_with ∥s∥₊ (has_scalar.smul s)

theorem norm_smul_of_nonneg {β : Type u_2} [semi_normed_group β] [normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :

∥t • x∥ = t * ∥x∥

theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_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} [semi_normed_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} [semi_normed_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} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

closure (metric.ball x r) = metric.closed_ball x r

theorem frontier_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

frontier (metric.ball x r) = metric.sphere x r

theorem interior_closed_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

interior (metric.closed_ball x r) = metric.ball x r

theorem frontier_closed_ball {E : Type u_5} [semi_normed_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

frontier (metric.closed_ball x r) = metric.sphere x r

theorem homeomorph_unit_ball_apply_coe {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] (x : E) :

↑(⇑homeomorph_unit_ball x) = (1 + ∥x∥)⁻¹ • x

noncomputable def homeomorph_unit_ball {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] :

E ≃ₜ ↥(metric.ball 0 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].

Equations

homeomorph_unit_ball = {to_equiv := {to_fun := λ (x : E), ⟨(1 + ∥x∥)⁻¹ • x, _⟩, inv_fun := λ (x : ↥(metric.ball 0 1)), (1 - ∥↑x∥)⁻¹ • ↑x, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

theorem homeomorph_unit_ball_symm_apply {E : Type u_1} [semi_normed_group E] [normed_space ℝ E] (x : ↥(metric.ball 0 1)) :

⇑(homeomorph_unit_ball.symm) x = (1 - ∥↑x∥)⁻¹ • ↑x

@[protected, instance]

def ulift.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] :

normed_space α (ulift E)

Equations

ulift.normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action ulift.module', add_smul := _, zero_smul := _}, norm_smul_le := _}

@[protected, instance]

def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [semi_normed_group E] [normed_space α E] {F : Type u_6} [semi_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

prod.normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action prod.module, add_smul := _, zero_smul := _}, norm_smul_le := _}

@[protected, instance]

def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), semi_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

pi.normed_space = {to_module := pi.module ι (λ (i : ι), E i) α (λ (i : ι), normed_space.to_module), norm_smul_le := _}

@[protected, instance]

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

normed_space 𝕜 ↥s

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

Equations

s.normed_space = {to_module := s.module' _inst_13, norm_smul_le := _}

theorem rescale_to_shell_semi_normed {α : Type u_1} [normed_field α] {E : Type u_5} [semi_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 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_group F] [normed_space α F] :

While this may appear identical to normed_space.to_module, it contains an implicit argument involving normed_group.to_semi_normed_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_group (E i)] [Π i, normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

This Zulip thread gives some more context.

Equations

normed_space.to_module' = normed_space.to_module

theorem exists_norm_eq (E : Type u_5) [normed_group E] [normed_space ℝ E] [nontrivial E] {c : ℝ} (hc : 0 ≤ c) :

∃ (x : E), ∥x∥ = c

@[simp]

theorem range_norm (E : Type u_5) [normed_group E] [normed_space ℝ E] [nontrivial E] :

set.range has_norm.norm = set.Ici 0

theorem nnnorm_surjective (E : Type u_5) [normed_group E] [normed_space ℝ E] [nontrivial E] :

function.surjective has_nnnorm.nnnorm

@[simp]

theorem range_nnnorm (E : Type u_5) [normed_group E] [normed_space ℝ E] [nontrivial E] :

set.range has_nnnorm.nnnorm = set.univ

theorem interior_closed_ball' {E : Type u_5} [normed_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

interior (metric.closed_ball x r) = metric.ball x r

theorem frontier_closed_ball' {E : Type u_5} [normed_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

frontier (metric.closed_ball x r) = metric.sphere x 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.

theorem normed_space.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] (c : ℝ) :

∃ (x : E), c < ∥x∥

If E is a nontrivial normed space over a nondiscrete 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) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] :

¬metric.bounded set.univ

@[protected]

theorem normed_space.noncompact_space (𝕜 : Type u_5) (E : Type u_6) [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] :

noncompact_space E

A normed vector space over a nondiscrete 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 nondiscrete_normed_field.noncompact_space (𝕜 : Type u_5) [nondiscrete_normed_field 𝕜] :

noncompact_space 𝕜

@[protected, instance]

def real_normed_space.noncompact_space (E : Type u_6) [normed_group E] [nontrivial E] [normed_space ℝ E] :

noncompact_space E

@[class]

structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :

Type (max u_5 u_6)

to_algebra : algebra 𝕜 𝕜'
norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥

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

normed_algebra.to_normed_space 𝕜' = {to_module := algebra.to_module normed_algebra.to_algebra, norm_smul_le := _}

@[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

normed_algebra.to_normed_space' = normed_algebra.to_normed_space 𝕜'

theorem norm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥ * ∥1∥

theorem nnnorm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥₊ = ∥x∥₊ * ∥1∥₊

@[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 : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥₊ = ∥x∥₊

theorem algebra_map_isometry (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] :

isometry ⇑(algebra_map 𝕜 𝕜')

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 𝕜'] [normed_algebra 𝕜 𝕜'] (ᾰ : 𝕜) :

⇑↑(algebra_map_clm 𝕜 𝕜') ᾰ = ⇑(algebra_map 𝕜 𝕜') ᾰ

def algebra_map_clm (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

𝕜 →L[𝕜] 𝕜'

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

Equations

algebra_map_clm 𝕜 𝕜' = {to_linear_map := {to_fun := ⇑(algebra_map 𝕜 𝕜'), map_add' := _, map_smul' := _}, cont := _}

@[simp]

theorem algebra_map_clm_apply (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (ᾰ : 𝕜) :

⇑(algebra_map_clm 𝕜 𝕜') ᾰ = ⇑(algebra_map 𝕜 𝕜') ᾰ

theorem algebra_map_clm_coe (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

⇑(algebra_map_clm 𝕜 𝕜') = ⇑(algebra_map 𝕜 𝕜')

theorem algebra_map_clm_to_linear_map (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

(algebra_map_clm 𝕜 𝕜').to_linear_map = algebra.linear_map 𝕜 𝕜'

@[protected, instance]

def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :

normed_algebra 𝕜 𝕜

Equations

normed_algebra.id 𝕜 = {to_algebra := {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := algebra.to_ring_hom (algebra.id 𝕜), commutes' := _, smul_def' := _}, norm_smul_le := _}

@[protected, instance]

def normed_algebra_rat {𝕜 : Type u_1} [normed_division_ring 𝕜] [char_zero 𝕜] [normed_algebra ℝ 𝕜] :

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

normed_algebra_rat = {to_algebra := algebra_rat _inst_5, norm_smul_le := _}

@[protected, instance]

def punit.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] :

normed_algebra 𝕜 punit

Equations

punit.normed_algebra 𝕜 = {to_algebra := punit.algebra (semifield.to_comm_semiring 𝕜), norm_smul_le := _}

@[protected, instance]

def ulift.normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

normed_algebra 𝕜 (ulift 𝕜')

Equations

ulift.normed_algebra 𝕜 𝕜' = {to_algebra := ulift.algebra normed_algebra.to_algebra, norm_smul_le := _}

@[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

prod.normed_algebra 𝕜 = {to_algebra := prod.algebra 𝕜 E F normed_algebra.to_algebra, norm_smul_le := _}

@[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 : ι), 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

pi.normed_algebra 𝕜 = {to_algebra := {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := algebra.to_ring_hom (pi.algebra ι E), commutes' := _, smul_def' := _}, norm_smul_le := _}

@[protected, instance]

def restrict_scalars.semi_normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : semi_normed_group E] :

semi_normed_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.semi_normed_group = I

@[protected, instance]

def restrict_scalars.normed_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_group E] :

normed_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.normed_group = I

@[protected, instance]

def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [semi_normed_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

restrict_scalars.normed_space 𝕜 𝕜' E = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action (restrict_scalars.module 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}

def module.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [semi_normed_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

module.restrict_scalars.normed_space_orig = I

def normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [semi_normed_group E] [normed_space 𝕜' 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

normed_space.restrict_scalars 𝕜 𝕜' E = restrict_scalars.normed_space 𝕜 𝕜' E