Normed spaces #
In this file we define (semi)normed spaces and algebras. We also prove some theorems about these definitions.
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
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โ
innorm_smul
.Note that since this requires
SeminormedAddCommGroup
and notNormedAddCommGroup
, this typeclass can be used for "semi normed spaces" too, just asModule
can be used for "semi modules".
Instances
Equations
- NormedField.toNormedSpace = NormedSpace.mk โฏ
Equations
- ULift.normedSpace = NormedSpace.mk โฏ
The product of two normed spaces is a normed space, with the sup norm.
Equations
- Prod.normedSpace = NormedSpace.mk โฏ
The product of finitely many normed spaces is a normed space, with the sup norm.
Equations
- Pi.normedSpace = NormedSpace.mk โฏ
Equations
- SeparationQuotient.instNormedSpace = NormedSpace.mk โฏ
Equations
- MulOpposite.instNormedSpace = NormedSpace.mk โฏ
A subspace of a normed space is also a normed space, with the restriction of the norm.
Equations
- s.normedSpace = NormedSpace.mk โฏ
Equations
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 = NormedSpace.mk โฏ
Instances For
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
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
.
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 ๐ = โ
.
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 : ๐ โ ๐'
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
Equations
- NormedAlgebra.toNormedSpace ๐' = NormedSpace.mk โฏ
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
This is a simpler version of norm_algebraMap
when โ1โ = 1
in ๐'
.
This is a simpler version of nnnorm_algebraMap
when โ1โ = 1
in ๐'
.
This is a simpler version of dist_algebraMap
when โ1โ = 1
in ๐'
.
In a normed algebra, the inclusion of the base field in the extended field is an isometry.
Equations
- NormedAlgebra.id ๐ = NormedAlgebra.mk โฏ
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 โฏ
Equations
- PUnit.normedAlgebra ๐ = NormedAlgebra.mk โฏ
Equations
- instNormedAlgebraULift ๐ ๐' = NormedAlgebra.mk โฏ
The product of two normed algebras is a normed algebra, with the sup norm.
Equations
- Prod.normedAlgebra ๐ = NormedAlgebra.mk โฏ
The product of finitely many normed algebras is a normed algebra, with the sup norm.
Equations
- Pi.normedAlgebra ๐ = NormedAlgebra.mk โฏ
Equations
Equations
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
Equations
- S.toNormedAlgebra = NormedAlgebra.induced ๐ (โฅS) A S.val
Equations
Equations
- instSeminormedAddCommGroupRestrictScalars = I
Equations
- instNormedAddCommGroupRestrictScalars = I
Equations
- instNonUnitalSeminormedRingRestrictScalars = I
Equations
- instNonUnitalNormedRingRestrictScalars = I
Equations
- instSeminormedRingRestrictScalars = I
Equations
- instNormedRingRestrictScalars = I
Equations
- instNonUnitalSeminormedCommRingRestrictScalars = I
Equations
- instNonUnitalNormedCommRingRestrictScalars = I
Equations
- instSeminormedCommRingRestrictScalars = I
Equations
- instNormedCommRingRestrictScalars = I
If E
is a normed space over ๐'
and ๐
is a normed algebra over ๐'
, then
RestrictScalars.module
is additionally a NormedSpace
.
Equations
- RestrictScalars.normedSpace ๐ ๐' E = NormedSpace.mk โฏ
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
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
If E
is a normed algebra over ๐'
and ๐
is a normed algebra over ๐'
, then
RestrictScalars.module
is additionally a NormedAlgebra
.
Equations
- RestrictScalars.normedAlgebra ๐ ๐' E = NormedAlgebra.mk โฏ
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
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.
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.
Instances For
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
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
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
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
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
Instances For
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
Instances For
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
- SeminormedAddCommGroup.ofCoreReplaceAll core HU HB = SeminormedAddCommGroup.mk โฏ
Instances For
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.
Instances For
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
Instances For
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
Instances For
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
- NormedAddCommGroup.ofCoreReplaceAll core HU HB = NormedAddCommGroup.mk โฏ
Instances For
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 = NormedSpace.mk โฏ