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 "seminormed spaces" too, just as Module can be used for "semimodules".

• smul : 𝕜 → E → E
• mul_smul (x y : 𝕜) (b : E) : (x * y) • b = x • y • b
• one_smul (b : E) : 1 • b = 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 "seminormed spaces" too, just as Module can be used for "semimodules".

theorem NormedSpace.ext {𝕜 : Type u_6} {E : Type u_7} {inst✝ : NormedField 𝕜} {inst✝¹ : SeminormedAddCommGroup E} {x y : NormedSpace 𝕜 E} (smul : SMul.smul = SMul.smul) : x = y

theorem NormedSpace.ext_iff {𝕜 : Type u_6} {E : Type u_7} {inst✝ : NormedField 𝕜} {inst✝¹ : SeminormedAddCommGroup E} {x y : NormedSpace 𝕜 E} : x = y ↔ SMul.smul = SMul.smul

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

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‖

@[simp]

theorem norm_natCast {α : Type u_6} [SeminormedRing α] [NormOneClass α] [NormSMulClass ℤ α] (a : ℕ) : ‖↑a‖ = ↑a

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)

theorem Metric.diam_sphere_eq {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) : diam (sphere x r) = 2 * r

theorem Metric.diam_closedBall_eq {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) : diam (closedBall x r) = 2 * r

theorem Metric.diam_ball_eq {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) : diam (ball x r) = 2 * r

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

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.

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.

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

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

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.

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

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

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

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

@[instance 100]

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

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 Algebra.norm_smul_one_eq_norm {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖x • 1‖ = ‖x‖

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

@[simp]

theorem tendsto_algebraMap_cobounded (𝕜 : Type u_6) (𝕜' : Type u_7) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : Filter.Tendsto (⇑(algebraMap 𝕜 𝕜')) (Bornology.cobounded 𝕜) (Bornology.cobounded 𝕜')

Preimages of cobounded sets under the algebra map are cobounded.

@[deprecated tendsto_algebraMap_cobounded (since := "2025-11-04")]

theorem algebraMap_cobounded_le_cobounded (𝕜 : Type u_6) (𝕜' : Type u_7) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : Filter.Tendsto (⇑(algebraMap 𝕜 𝕜')) (Bornology.cobounded 𝕜) (Bornology.cobounded 𝕜')

Alias of tendsto_algebraMap_cobounded.

---

Preimages of cobounded sets under the algebra map are cobounded.

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 𝕜 𝕜

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.

instance PUnit.normedAlgebra (𝕜 : Type u_1) [NormedField 𝕜] : NormedAlgebra 𝕜 PUnit.{u_6 + 1}

instance instNormedAlgebraULift (𝕜 : Type u_1) (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] : NormedAlgebra 𝕜 (ULift.{u_6, u_2} 𝕜')

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.

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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.

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

theorem NormedSpace.restrictScalars_eq (𝕜 : Type u_1) (𝕜' : Type u_2) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_6} [SeminormedAddCommGroup E] [h : NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : restrictScalars 𝕜 𝕜' E = h

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.

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.

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

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 SeminormedSpace.Core (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] : Prop

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

@[reducible, inline]

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

Produces a PseudoMetricSpace E instance from a SeminormedSpace.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].

@[reducible, inline]

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

Produces a PseudoEMetricSpace E instance from a SeminormedSpace.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].

@[reducible, inline]

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

Produces a PseudoEMetricSpace E instance from a SeminormedSpace.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].

@[reducible, inline]

abbrev PseudoMetricSpace.ofSeminormedSpaceCoreReplaceTopology {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [T : TopologicalSpace E] (core : SeminormedSpace.Core 𝕜 E) (H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace) : PseudoMetricSpace E

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

@[reducible, inline]

abbrev PseudoMetricSpace.ofSeminormedSpaceCoreReplaceAll {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [U : UniformSpace E] [B : Bornology E] (core : SeminormedSpace.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 SeminormedSpace.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].

@[reducible, inline]

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

Produces a SeminormedAddCommGroup E instance from a SeminormedSpace.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].

@[reducible, inline]

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

Produces a SeminormedAddCommGroup E instance from a SeminormedSpace.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].

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofCoreReplaceTopology {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E] [T : TopologicalSpace E] (core : SeminormedSpace.Core 𝕜 E) (H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace) : SeminormedAddCommGroup E

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

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

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

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

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

@[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 NormedSpace.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].

@[reducible, inline]

abbrev NormedAddCommGroup.ofCoreReplaceTopology {𝕜 : Type u_6} {E : Type u_7} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Norm E] [T : TopologicalSpace E] (core : NormedSpace.Core 𝕜 E) (H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace) : NormedAddCommGroup E

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

@[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 NormedSpace.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].

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

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.