Documentation

Mathlib.Analysis.NormedSpace.Basic

Normed spaces #

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

class NormedSpace (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] extends Module :

Type (max u_6 u_7)

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 SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "semi normed spaces" too, just as Module can be used for "semi modules".

smul : 𝕜 → E → E
one_smul : ∀ (b : E), 1 • b = b
mul_smul : ∀ (x y : 𝕜) (b : E), (x * y) • b = x • y • b
smul_zero : ∀ (a : 𝕜), a • 0 = 0
smul_add : ∀ (a : 𝕜) (x y : E), a • (x + y) = a • x + a • y
add_smul : ∀ (r s : 𝕜) (x : E), (r + s) • x = r • x + s • x
zero_smul : ∀ (x : E), 0 • x = 0
norm_smul_le : ∀ (a : 𝕜) (b : E), ‖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 SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "semi normed spaces" too, just as Module can be used for "semi modules".

Instances

instance NormedSpace.boundedSMul {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :

BoundedSMul 𝕜 E

Equations

⋯ = ⋯

instance NormedField.toNormedSpace {𝕜 : Type u_1} [NormedField 𝕜] :

NormedSpace 𝕜 𝕜

Equations

NormedField.toNormedSpace = NormedSpace.mk ⋯

instance NormedField.to_boundedSMul {𝕜 : Type u_1} [NormedField 𝕜] :

BoundedSMul 𝕜 𝕜

Equations

⋯ = ⋯

theorem norm_zsmul (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (n : ℤ) (x : E) :

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

theorem eventually_nhds_norm_smul_sub_lt {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) :

∀ᶠ (y : E) in nhds x, ‖c • (y - x)‖ < ε

theorem Filter.Tendsto.zero_smul_isBoundedUnder_le {𝕜 : Type u_1} {E : Type u_3} {α : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) :

Filter.Tendsto (fun (x : α) => f x • g x) l (nhds 0)

theorem Filter.IsBoundedUnder.smul_tendsto_zero {𝕜 : Type u_1} {E : Type u_3} {α : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α} (hf : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ f)) (hg : Filter.Tendsto g l (nhds 0)) :

Filter.Tendsto (fun (x : α) => f x • g x) l (nhds 0)

instance NormedSpace.discreteTopology_zmultiples {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :

DiscreteTopology ↥(AddSubgroup.zmultiples e)

Equations

⋯ = ⋯

instance ULift.normedSpace {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :

NormedSpace 𝕜 (ULift.{u_6, u_3} E)

Equations

ULift.normedSpace = let __spread.0 := ULift.seminormedAddCommGroup; let __spread.1 := ULift.module'; NormedSpace.mk ⋯

instance Prod.normedSpace {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] :

NormedSpace 𝕜 (E × F)

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

Equations

Prod.normedSpace = let __src := Prod.seminormedAddCommGroup; let __src := Prod.instModule; NormedSpace.mk ⋯

instance Pi.normedSpace {𝕜 : Type u_1} [NormedField 𝕜] {ι : Type u_6} {E : ι → Type u_7} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] :

NormedSpace 𝕜 ((i : ι) → E i)

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

Equations

Pi.normedSpace = NormedSpace.mk ⋯

instance MulOpposite.instNormedSpace {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :

NormedSpace 𝕜 Eᵐᵒᵖ

Equations

MulOpposite.instNormedSpace = NormedSpace.mk ⋯

instance Submodule.normedSpace {𝕜 : Type u_6} {R : Type u_7} [SMul 𝕜 R] [NormedField 𝕜] [Ring R] {E : Type u_8} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Module R E] [IsScalarTower 𝕜 R E] (s : Submodule R E) :

NormedSpace 𝕜 ↥s

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

Equations

Submodule.normedSpace s = NormedSpace.mk ⋯

@[reducible]

def NormedSpace.induced {F : Type u_6} (𝕜 : Type u_7) (E : Type u_8) (G : Type u_9) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [FunLike F E G] [LinearMapClass F 𝕜 E G] (f : F) :

NormedSpace 𝕜 E

A linear map from a Module to a NormedSpace induces a NormedSpace structure on the domain, using the SeminormedAddCommGroup.induced norm.

See note [reducible non-instances]

Equations

NormedSpace.induced 𝕜 E G f = let x := SeminormedAddCommGroup.induced E G f; NormedSpace.mk ⋯

Instances For

instance NormedSpace.toModule' {𝕜 : Type u_1} {F : Type u_4} [NormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :

Module 𝕜 F

While this may appear identical to NormedSpace.toModule, it contains an implicit argument involving NormedAddCommGroup.toSeminormedAddCommGroup that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this NormedSpace.toModule':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [NormedField 𝕜] [Π i, NormedAddCommGroup (E i)] [Π i, NormedSpace 𝕜 (E i)] :
  Π i, Module 𝕜 (E i) := by infer_instance

This Zulip thread gives some more context.

Equations

NormedSpace.toModule' = NormedSpace.toModule

theorem NormedSpace.exists_lt_norm (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 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.

theorem NormedSpace.unbounded_univ (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :

¬Bornology.IsBounded Set.univ

theorem NormedSpace.cobounded_neBot (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :

Filter.NeBot (Bornology.cobounded E)

instance NontriviallyNormedField.cobounded_neBot (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] :

Filter.NeBot (Bornology.cobounded 𝕜)

Equations

⋯ = ⋯

instance RealNormedSpace.cobounded_neBot (E : Type u_3) [NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E] :

Filter.NeBot (Bornology.cobounded E)

Equations

⋯ = ⋯

instance NontriviallyNormedField.infinite (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] :

Equations

⋯ = ⋯

theorem NormedSpace.noncompactSpace (𝕜 : Type u_1) (E : Type u_3) [NormedField 𝕜] [Infinite 𝕜] [NormedAddCommGroup E] [Nontrivial E] [NormedSpace 𝕜 E] :

NoncompactSpace E

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

instance NormedField.noncompactSpace (𝕜 : Type u_1) [NormedField 𝕜] [Infinite 𝕜] :

NoncompactSpace 𝕜

Equations

⋯ = ⋯

instance RealNormedSpace.noncompactSpace (E : Type u_3) [NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E] :

NoncompactSpace E

Equations

⋯ = ⋯

class NormedAlgebra (𝕜 : Type u_6) (𝕜' : Type u_7) [NormedField 𝕜] [SeminormedRing 𝕜'] extends Algebra :

Type (max u_6 u_7)

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:

variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']

smul : 𝕜 → 𝕜' → 𝕜'
toFun : 𝕜 → 𝕜'
map_one' : Algebra.toRingHom.toFun 1 = 1
map_mul' : ∀ (x y : 𝕜), Algebra.toRingHom.toFun (x * y) = Algebra.toRingHom.toFun x * Algebra.toRingHom.toFun y
map_zero' : Algebra.toRingHom.toFun 0 = 0
map_add' : ∀ (x y : 𝕜), Algebra.toRingHom.toFun (x + y) = Algebra.toRingHom.toFun x + Algebra.toRingHom.toFun y
commutes' : ∀ (r : 𝕜) (x : 𝕜'), Algebra.toRingHom r * x = x * Algebra.toRingHom r
smul_def' : ∀ (r : 𝕜) (x : 𝕜'), r • x = Algebra.toRingHom r * x
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:
```
variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
```

Instances

instance NormedAlgebra.toNormedSpace {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

NormedSpace 𝕜 𝕜'

Equations

NormedAlgebra.toNormedSpace 𝕜' = let __src := Algebra.toModule; NormedSpace.mk ⋯

instance NormedAlgebra.toNormedSpace' {𝕜 : Type u_1} [NormedField 𝕜] {𝕜' : Type u_6} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

NormedSpace 𝕜 𝕜'

While this may appear identical to NormedAlgebra.toNormedSpace, it contains an implicit argument involving NormedRing.toSeminormedRing that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this NormedSpace.toModule':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [NormedField 𝕜] [Π i, NormedRing (E i)] [Π i, NormedAlgebra 𝕜 (E i)] :
  Π i, Module 𝕜 (E i) := by infer_instance

See NormedSpace.toModule' for a similar situation.

Equations

NormedAlgebra.toNormedSpace' = inferInstance

theorem norm_algebraMap {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (x : 𝕜) :

‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

theorem nnnorm_algebraMap {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (x : 𝕜) :

‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊ * ‖1‖₊

@[simp]

theorem norm_algebraMap' {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) :

‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖

@[simp]

theorem nnnorm_algebraMap' {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) :

‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊

@[simp]

theorem norm_algebraMap_nnreal (𝕜' : Type u_2) [SeminormedRing 𝕜'] [NormOneClass 𝕜'] [NormedAlgebra ℝ 𝕜'] (x : NNReal) :

‖(algebraMap NNReal 𝕜') x‖ = ↑x

@[simp]

theorem nnnorm_algebraMap_nnreal (𝕜' : Type u_2) [SeminormedRing 𝕜'] [NormOneClass 𝕜'] [NormedAlgebra ℝ 𝕜'] (x : NNReal) :

‖(algebraMap NNReal 𝕜') x‖₊ = x

theorem algebraMap_isometry (𝕜 : Type u_1) (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] :

Isometry ⇑(algebraMap 𝕜 𝕜')

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

instance NormedAlgebra.id (𝕜 : Type u_1) [NormedField 𝕜] :

NormedAlgebra 𝕜 𝕜

Equations

NormedAlgebra.id 𝕜 = let __src := NormedField.toNormedSpace; let __src_1 := Algebra.id 𝕜; NormedAlgebra.mk ⋯

instance normedAlgebraRat {𝕜 : Type u_6} [NormedDivisionRing 𝕜] [CharZero 𝕜] [NormedAlgebra ℝ 𝕜] :

NormedAlgebra ℚ 𝕜

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 AlgebraRat respects that norm.

Equations

normedAlgebraRat = NormedAlgebra.mk ⋯

instance PUnit.normedAlgebra (𝕜 : Type u_1) [NormedField 𝕜] :

NormedAlgebra 𝕜 PUnit.{u_6 + 1}

Equations

PUnit.normedAlgebra 𝕜 = NormedAlgebra.mk ⋯

instance instNormedAlgebraULiftSeminormedRing (𝕜 : Type u_1) (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

NormedAlgebra 𝕜 (ULift.{u_6, u_2} 𝕜')

Equations

instNormedAlgebraULiftSeminormedRing 𝕜 𝕜' = let __src := ULift.normedSpace; let __src_1 := ULift.algebra; NormedAlgebra.mk ⋯

instance Prod.normedAlgebra (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_6} {F : Type u_7} [SeminormedRing E] [SeminormedRing F] [NormedAlgebra 𝕜 E] [NormedAlgebra 𝕜 F] :

NormedAlgebra 𝕜 (E × F)

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

Equations

Prod.normedAlgebra 𝕜 = let __src := Prod.normedSpace; let __src_1 := Prod.algebra 𝕜 E F; NormedAlgebra.mk ⋯

instance Pi.normedAlgebra (𝕜 : Type u_1) [NormedField 𝕜] {ι : Type u_6} {E : ι → Type u_7} [Fintype ι] [(i : ι) → SeminormedRing (E i)] [(i : ι) → NormedAlgebra 𝕜 (E i)] :

NormedAlgebra 𝕜 ((i : ι) → E i)

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

Equations

Pi.normedAlgebra 𝕜 = let __src := Pi.normedSpace; let __src_1 := Pi.algebra ι E; NormedAlgebra.mk ⋯

instance MulOpposite.instNormedAlgebra (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_6} [SeminormedRing E] [NormedAlgebra 𝕜 E] :

NormedAlgebra 𝕜 Eᵐᵒᵖ

Equations

MulOpposite.instNormedAlgebra 𝕜 = let __spread.0 := MulOpposite.instAlgebra; let __spread.1 := MulOpposite.instNormedSpace; NormedAlgebra.mk ⋯

@[reducible]

def NormedAlgebra.induced {F : Type u_6} (𝕜 : Type u_7) (R : Type u_8) (S : Type u_9) [NormedField 𝕜] [Ring R] [Algebra 𝕜 R] [SeminormedRing S] [NormedAlgebra 𝕜 S] [FunLike F R S] [NonUnitalAlgHomClass F 𝕜 R S] (f : F) :

NormedAlgebra 𝕜 R

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

See note [reducible non-instances]

Equations

NormedAlgebra.induced 𝕜 R S f = NormedAlgebra.mk ⋯

Instances For

instance Subalgebra.toNormedAlgebra {𝕜 : Type u_6} {A : Type u_7} [SeminormedRing A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] (S : Subalgebra 𝕜 A) :

NormedAlgebra 𝕜 ↥S

Equations

Subalgebra.toNormedAlgebra S = NormedAlgebra.induced 𝕜 (↥S) A (Subalgebra.val S)

instance instSeminormedAddCommGroupRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : SeminormedAddCommGroup E] :

SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)

Equations

instSeminormedAddCommGroupRestrictScalars = I

instance instNormedAddCommGroupRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NormedAddCommGroup E] :

NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)

Equations

instNormedAddCommGroupRestrictScalars = I

instance instNonUnitalSeminormedRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NonUnitalSeminormedRing E] :

NonUnitalSeminormedRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNonUnitalSeminormedRingRestrictScalars = I

instance instNonUnitalNormedRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NonUnitalNormedRing E] :

NonUnitalNormedRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNonUnitalNormedRingRestrictScalars = I

instance instSeminormedRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : SeminormedRing E] :

SeminormedRing (RestrictScalars 𝕜 𝕜' E)

Equations

instSeminormedRingRestrictScalars = I

instance instNormedRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NormedRing E] :

NormedRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNormedRingRestrictScalars = I

instance instNonUnitalSeminormedCommRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NonUnitalSeminormedCommRing E] :

NonUnitalSeminormedCommRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNonUnitalSeminormedCommRingRestrictScalars = I

instance instNonUnitalNormedCommRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NonUnitalNormedCommRing E] :

NonUnitalNormedCommRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNonUnitalNormedCommRingRestrictScalars = I

instance instSeminormedCommRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : SeminormedCommRing E] :

SeminormedCommRing (RestrictScalars 𝕜 𝕜' E)

Equations

instSeminormedCommRingRestrictScalars = I

instance instNormedCommRingRestrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : NormedCommRing E] :

NormedCommRing (RestrictScalars 𝕜 𝕜' E)

Equations

instNormedCommRingRestrictScalars = I

instance RestrictScalars.normedSpace (𝕜 : Type u_1) (𝕜' : Type u_2) (E : Type u_3) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜' E] :

NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E)

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

Equations

RestrictScalars.normedSpace 𝕜 𝕜' E = let __src := RestrictScalars.module 𝕜 𝕜' E; NormedSpace.mk ⋯

def Module.RestrictScalars.normedSpaceOrig {𝕜 : Type u_6} {𝕜' : Type u_7} {E : Type u_8} [NormedField 𝕜'] [SeminormedAddCommGroup E] [I : NormedSpace 𝕜' E] :

NormedSpace 𝕜' (RestrictScalars 𝕜 𝕜' E)

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

Equations

Module.RestrictScalars.normedSpaceOrig = I

Instances For

def NormedSpace.restrictScalars (𝕜 : Type u_1) (𝕜' : Type u_2) (E : Type u_3) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜' E] :

NormedSpace 𝕜 E

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

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

Equations

NormedSpace.restrictScalars 𝕜 𝕜' E = RestrictScalars.normedSpace 𝕜 𝕜' E

Instances For

instance RestrictScalars.normedAlgebra (𝕜 : Type u_1) (𝕜' : Type u_2) (E : Type u_3) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedRing E] [NormedAlgebra 𝕜' E] :

NormedAlgebra 𝕜 (RestrictScalars 𝕜 𝕜' E)

If E is a normed algebra over 𝕜' and 𝕜 is a normed algebra over 𝕜', then RestrictScalars.module is additionally a NormedAlgebra.

Equations

RestrictScalars.normedAlgebra 𝕜 𝕜' E = let __src := RestrictScalars.algebra 𝕜 𝕜' E; NormedAlgebra.mk ⋯

def Module.RestrictScalars.normedAlgebraOrig {𝕜 : Type u_6} {𝕜' : Type u_7} {E : Type u_8} [NormedField 𝕜'] [SeminormedRing E] [I : NormedAlgebra 𝕜' E] :

NormedAlgebra 𝕜' (RestrictScalars 𝕜 𝕜' E)

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

Equations

Module.RestrictScalars.normedAlgebraOrig = I

Instances For

def NormedAlgebra.restrictScalars (𝕜 : Type u_1) (𝕜' : Type u_2) (E : Type u_3) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedRing E] [NormedAlgebra 𝕜' E] :

NormedAlgebra 𝕜 E

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

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

Equations

NormedAlgebra.restrictScalars 𝕜 𝕜' E = RestrictScalars.normedAlgebra 𝕜 𝕜' E

Instances For