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)

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

has_bounded_smul α β

@[protected, instance]

def real.module :

Equations

real.module = semiring.to_module

@[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 α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :

‖s • x‖ = ‖s‖ * ‖x‖

theorem norm_zsmul {β : Type u_2} [seminormed_add_comm_group β] (α : Type u_1) [normed_field α] [normed_space α β] (n : ℤ) (x : β) :

‖n • x‖ = ‖↑n‖ * ‖x‖

@[simp]

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

|‖z‖| = ‖z‖

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

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

theorem dist_smul₀ {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_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 α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :

‖s • x‖₊ = ‖s‖₊ * ‖x‖₊

theorem nndist_smul₀ {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_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 α] [seminormed_add_comm_group β] [normed_space α β] (s : α) :

lipschitz_with ‖s‖₊ (has_smul.smul s)

theorem norm_smul_of_nonneg {β : Type u_2} [seminormed_add_comm_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} [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) :

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

theorem frontier_ball {E : Type u_5} [seminormed_add_comm_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} [seminormed_add_comm_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} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

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

@[protected, instance]

def add_subgroup.zmultiples.discrete_topology {E : Type u_1} [normed_add_comm_group E] [normed_space ℚ E] (e : E) :

discrete_topology ↥(add_subgroup.zmultiples e)

theorem homeomorph_unit_ball_apply_coe {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) :

↑(⇑homeomorph_unit_ball x) = (real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x

noncomputable def homeomorph_unit_ball {E : Type u_5} [seminormed_add_comm_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].

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

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

theorem homeomorph_unit_ball_symm_apply {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (y : ↥(metric.ball 0 1)) :

⇑(homeomorph_unit_ball.symm) y = (real.sqrt (1 - ‖↑y‖ ^ 2))⁻¹ • ↑y

@[simp]

theorem coe_homeomorph_unit_ball_apply_zero {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] :

↑(⇑homeomorph_unit_ball 0) = 0

@[protected, instance]

def ulift.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_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} [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

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

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

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} [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.

@[reducible]

def normed_space.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [add_comm_group β] [module α β] [seminormed_add_comm_group γ] [normed_space α γ] [linear_map_class F α β γ] (f : F) :

normed_space α β

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.

See note [reducible non-instances]

Equations

normed_space.induced α β γ f = {to_module := _inst_3, norm_smul_le := _}

@[protected, instance]

def normed_space.to_module' {α : Type u_1} [normed_field α] {F : Type u_6} [normed_add_comm_group F] [normed_space α 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

normed_space.to_module' = normed_space.to_module

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

@[simp]

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

set.range has_norm.norm = set.Ici 0

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

function.surjective has_nnnorm.nnnorm

@[simp]

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

set.range has_nnnorm.nnnorm = set.univ

@[protected, instance]

def real.punctured_nhds_module_ne_bot {E : Type u_1} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E] [module ℝ E] [has_continuous_smul ℝ E] (x : E) :

(nhds_within x {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} [normed_add_comm_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_add_comm_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_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]

theorem normed_space.unbounded_univ (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] :

¬metric.bounded set.univ

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

noncompact_space 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) [nontrivially_normed_field 𝕜] :

noncompact_space 𝕜

@[protected, instance]

def real_normed_space.noncompact_space (E : Type u_6) [normed_add_comm_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‖₊

@[simp]

theorem norm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :

‖⇑(algebra_map nnreal 𝕜') x‖ = ↑x

@[simp]

theorem nnnorm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :

‖⇑(algebra_map nnreal 𝕜') 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.

@[protected, instance]

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

normed_algebra 𝕜 𝕜

Equations

normed_algebra.id 𝕜 = {to_algebra := {to_has_smul := mul_action.to_has_smul 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]

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_smul := mul_action.to_has_smul distrib_mul_action.to_mul_action, to_ring_hom := algebra.to_ring_hom (pi.algebra ι E), commutes' := _, smul_def' := _}, norm_smul_le := _}

@[reducible]

def normed_algebra.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [ring β] [algebra α β] [semi_normed_ring γ] [normed_algebra α γ] [non_unital_alg_hom_class F α β γ] (f : F) :

normed_algebra α β

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.

See note [reducible non-instances]

Equations

normed_algebra.induced α β γ f = {to_algebra := _inst_3, norm_smul_le := _}

@[protected, instance]

def subalgebra.to_normed_algebra {𝕜 : Type u_1} {A : Type u_2} [semi_normed_ring A] [normed_field 𝕜] [normed_algebra 𝕜 A] (S : subalgebra 𝕜 A) :

normed_algebra 𝕜 ↥S

Equations

S.to_normed_algebra = normed_algebra.induced 𝕜 ↥S A S.val

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

seminormed_add_comm_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.seminormed_add_comm_group = I

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

normed_add_comm_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.normed_add_comm_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) [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

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 𝕜'] [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

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) [seminormed_add_comm_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