Documentation

Mathlib.Analysis.Normed.Module.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 𝕜 E :

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 100]

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

NormSMulClass 𝕜 E

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

IsBoundedSMul 𝕜 E

This is a shortcut instance, which was found to help with performance in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Normed.20modules/near/516757412.

It is implied via NormedSpace.toNormSMulClass.

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

NormedSpace 𝕜 𝕜

Equations

NormedField.toNormedSpace = { toModule := Semiring.toModule, norm_smul_le := ⋯ }

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

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

theorem norm_intCast_eq_abs_mul_norm_one (α : Type u_6) [SeminormedRing α] [NormSMulClass ℤ α] (n : ℤ) :

‖↑n‖ = ↑|n| * ‖1‖

theorem norm_natCast_eq_mul_norm_one (α : Type u_6) [SeminormedRing α] [NormSMulClass ℤ α] (n : ℕ) :

‖↑n‖ = ↑n * ‖1‖

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 : Tendsto f l (nhds 0)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (Norm.norm ∘ g)) :

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 : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) (hg : Tendsto g l (nhds 0)) :

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)

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 = { toModule := ULift.module', norm_smul_le := ⋯ }

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 = { toModule := Prod.instModule, norm_smul_le := ⋯ }

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 = { toModule := Pi.module ι E 𝕜, norm_smul_le := ⋯ }

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

NormedSpace 𝕜 (SeparationQuotient E)

Equations

SeparationQuotient.instNormedSpace = { toModule := SeparationQuotient.instModule, norm_smul_le := ⋯ }

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

NormedSpace 𝕜 Eᵐᵒᵖ

Equations

MulOpposite.instNormedSpace = { toModule := MulOpposite.instModule 𝕜, norm_smul_le := ⋯ }

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

s.normedSpace = { toModule := s.module', norm_smul_le := ⋯ }

@[instance 75]

instance SubmoduleClass.toNormedSpace {S : Type u_6} {𝕜 : Type u_7} {R : Type u_8} {E : Type u_9} [SMul 𝕜 R] [NormedField 𝕜] [Ring R] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Module R E] [IsScalarTower 𝕜 R E] [SetLike S E] [AddSubgroupClass S E] [SMulMemClass S R E] (s : S) :

NormedSpace 𝕜 ↥s

Equations

SubmoduleClass.toNormedSpace s = { toModule := SubmoduleClass.module' s, norm_smul_le := ⋯ }

@[reducible, inline]

abbrev 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 = { toModule := inst✝⁴, norm_smul_le := ⋯ }

Instances For

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

(Bornology.cobounded E).NeBot

@[instance 100]

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

(Bornology.cobounded 𝕜).NeBot

@[instance 80]

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

(Bornology.cobounded E).NeBot

@[instance 80]

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

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 100]

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

NoncompactSpace 𝕜

@[instance 100]

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

NoncompactSpace E

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 : 𝕜 → 𝕜' → 𝕜'
algebraMap : 𝕜 →+* 𝕜'
commutes' (r : 𝕜) (x : 𝕜') : Algebra.algebraMap r * x = x * Algebra.algebraMap r
smul_def' (r : 𝕜) (x : 𝕜') : r • x = Algebra.algebraMap 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 100]

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

NormedSpace 𝕜 𝕜'

Equations

NormedAlgebra.toNormedSpace 𝕜' = { toModule := Algebra.toModule, norm_smul_le := ⋯ }

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‖₊

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

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

@[simp]

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

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

This is a simpler version of norm_algebraMap when ‖1‖ = 1 in 𝕜'.

@[simp]

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

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

This is a simpler version of nnnorm_algebraMap when ‖1‖ = 1 in 𝕜'.

@[simp]

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

dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y

This is a simpler version of dist_algebraMap when ‖1‖ = 1 in 𝕜'.

@[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 𝕜 = { toSMul := NormedField.toNormedSpace.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

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 = { toAlgebra := DivisionRing.toRatAlgebra, norm_smul_le := ⋯ }

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

NormedAlgebra 𝕜 PUnit.{u_6 + 1}

Equations

PUnit.normedAlgebra 𝕜 = { toAlgebra := PUnit.algebra, norm_smul_le := ⋯ }

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

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

Equations

instNormedAlgebraULift 𝕜 𝕜' = { toSMul := ULift.normedSpace.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

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 𝕜 = { toSMul := Prod.normedSpace.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

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 𝕜 = { toSMul := Pi.normedSpace.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

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

NormedAlgebra 𝕜 (SeparationQuotient E)

Equations

SeparationQuotient.instNormedAlgebra 𝕜 = { toSMul := inferInstance.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

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

NormedAlgebra 𝕜 Eᵐᵒᵖ

Equations

MulOpposite.instNormedAlgebra 𝕜 = { toAlgebra := MulOpposite.instAlgebra, norm_smul_le := ⋯ }

@[reducible, inline]

abbrev 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 = { toAlgebra := inst✝⁴, norm_smul_le := ⋯ }

Instances For

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

NormedAlgebra 𝕜 ↥S

Equations

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

@[instance 75]

instance SubalgebraClass.toNormedAlgebra {S : Type u_6} {𝕜 : Type u_7} {E : Type u_8} [NormedField 𝕜] [SeminormedRing E] [NormedAlgebra 𝕜 E] [SetLike S E] [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) :

NormedAlgebra 𝕜 ↥s

Equations

SubalgebraClass.toNormedAlgebra s = { toAlgebra := SubalgebraClass.toAlgebra s, norm_smul_le := ⋯ }

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 = { toModule := RestrictScalars.module 𝕜 𝕜' E, norm_smul_le := ⋯ }

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

@[reducible, inline]

abbrev 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.

See Note [reducible non-instances].

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 = { toAlgebra := RestrictScalars.algebra 𝕜 𝕜' E, norm_smul_le := ⋯ }

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

@[reducible, inline]

abbrev 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.

See Note [reducible non-instances].

Equations

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

Instances For

Structures for constructing new normed spaces #

This section contains tools meant for constructing new normed spaces. These allow one to easily construct all the relevant instances (distances measures, etc) while proving only a minimal set of axioms. Furthermore, tools are provided to add a norm structure to a type that already has a preexisting uniformity or bornology: in such cases, it is necessary to keep the preexisting instances, while ensuring that the norm induces the same uniformity/bornology.

structure SeminormedAddCommGroup.Core (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] :

A structure encapsulating minimal axioms needed to defined a seminormed vector space, as found in textbooks. This is meant to be used to easily define SeminormedAddCommGroup E instances from scratch on a type with no preexisting distance or topology.

norm_nonneg (x : E) : 0 ≤ ‖x‖
norm_smul (c : 𝕜) (x : E) : ‖c • x‖ = ‖c‖ * ‖x‖
norm_triangle (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

Instances For

@[reducible, inline]

abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCore {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] (core : SeminormedAddCommGroup.Core 𝕜 E) :

PseudoMetricSpace E

Produces a PseudoMetricSpace E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new uniformity and topology on the type. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev PseudoEMetricSpace.ofSeminormedAddCommGroupCore {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] (core : SeminormedAddCommGroup.Core 𝕜 E) :

PseudoEMetricSpace E

Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new uniformity and topology on the type. See note [reducible non-instances].

Equations

PseudoEMetricSpace.ofSeminormedAddCommGroupCore core = PseudoMetricSpace.toPseudoEMetricSpace

Instances For

@[reducible, inline]

abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceUniformity {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [U : UniformSpace E] (core : SeminormedAddCommGroup.Core 𝕜 E) (H : uniformity E = uniformity E) :

PseudoMetricSpace E

Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

Equations

PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceUniformity core H = (PseudoMetricSpace.ofSeminormedAddCommGroupCore core).replaceUniformity H

Instances For

@[reducible, inline]

abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceAll {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [U : UniformSpace E] [B : Bornology E] (core : SeminormedAddCommGroup.Core 𝕜 E) (HU : uniformity E = uniformity E) (HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) :

PseudoMetricSpace E

Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

Equations

PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceAll core HU HB = ((PseudoMetricSpace.ofSeminormedAddCommGroupCore core).replaceUniformity HU).replaceBornology HB

Instances For

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofCore {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] (core : Core 𝕜 E) :

SeminormedAddCommGroup E

Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new distance measure from the norm. it must therefore not be used on a type with a preexisting distance measure or topology. See note [reducible non-instances].

Equations

SeminormedAddCommGroup.ofCore core = { toNorm := inst✝¹, toAddCommGroup := inst✝², toPseudoMetricSpace := PseudoMetricSpace.ofSeminormedAddCommGroupCore core, dist_eq := ⋯ }

Instances For

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofCoreReplaceUniformity {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [U : UniformSpace E] (core : Core 𝕜 E) (H : uniformity E = uniformity E) :

SeminormedAddCommGroup E

Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofCoreReplaceAll {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [U : UniformSpace E] [B : Bornology E] (core : Core 𝕜 E) (HU : uniformity E = uniformity E) (HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) :

SeminormedAddCommGroup E

Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

structure NormedSpace.Core (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Norm E] extends SeminormedAddCommGroup.Core 𝕜 E :

A structure encapsulating minimal axioms needed to defined a normed vector space, as found in textbooks. This is meant to be used to easily define NormedAddCommGroup E and NormedSpace E instances from scratch on a type with no preexisting distance or topology.

norm_nonneg (x : E) : 0 ≤ ‖x‖
norm_smul (c : 𝕜) (x : E) : ‖c • x‖ = ‖c‖ * ‖x‖
norm_triangle (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖
norm_eq_zero_iff (x : E) : ‖x‖ = 0 ↔ x = 0

Instances For

@[reducible, inline]

abbrev NormedAddCommGroup.ofCore {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Norm E] (core : NormedSpace.Core 𝕜 E) :

NormedAddCommGroup E

Produces a NormedAddCommGroup E instance from a NormedSpace.Core. Note that if this is used to define an instance on a type, it also provides a new distance measure from the norm. it must therefore not be used on a type with a preexisting distance measure. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedAddCommGroup.ofCoreReplaceUniformity {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Norm E] [U : UniformSpace E] (core : NormedSpace.Core 𝕜 E) (H : uniformity E = uniformity E) :

NormedAddCommGroup E

Produces a NormedAddCommGroup E instance from a NormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedAddCommGroup.ofCoreReplaceAll {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Norm E] [U : UniformSpace E] [B : Bornology E] (core : NormedSpace.Core 𝕜 E) (HU : uniformity E = uniformity E) (HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) :

NormedAddCommGroup E

Produces a NormedAddCommGroup E instance from a NormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedSpace.ofCore {𝕜 : Type u_8} {E : Type u_9} [NormedField 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (core : Core 𝕜 E) :

NormedSpace 𝕜 E

Produces a NormedSpace 𝕜 E instance from a NormedSpace.Core. This is meant to be used on types where the NormedAddCommGroup E instance has also been defined using core. See note [reducible non-instances].

Equations

NormedSpace.ofCore core = { toModule := inst✝, norm_smul_le := ⋯ }

Instances For

theorem AddMonoidHom.continuous_of_isBounded_nhds_zero {G : Type u_6} {H : Type u_7} [SeminormedAddCommGroup G] [SeminormedAddCommGroup H] [NormedSpace ℝ H] {s : Set G} (f : G →+ H) (hs : s ∈ nhds 0) (hbounded : Bornology.IsBounded (⇑f '' s)) :

Continuous ⇑f

A group homomorphism from a normed group to a real normed space, bounded on a neighborhood of 0, must be continuous.