Finite dimensional normed spaces over complete fields #
Over a complete nontrivially normed field, in finite dimension, all norms are equivalent and all linear maps are continuous. Moreover, a finite-dimensional subspace is always complete and closed.
Main results: #
FiniteDimensional.complete: a finite-dimensional space over a complete field is complete. This is not registered as an instance, as the field would be an unknown metavariable in typeclass resolution.Submodule.closed_of_finiteDimensional: a finite-dimensional subspace over a complete field is closedFiniteDimensional.proper: a finite-dimensional space over a proper field is proper. This is not registered as an instance, as the field would be an unknown metavariable in typeclass resolution. It is however registered as an instance forπ = βandπ = β. As properness implies completeness, there is no need to also registerFiniteDimensional.completeonβorβ.FiniteDimensional.of_isCompact_closedBall: Riesz' theorem: if the closed unit ball is compact, then the space is finite-dimensional.
Implementation notes #
The fact that all norms are equivalent is not written explicitly, as it would mean having two norms
on a single space, which is not the way type classes work. However, if one has a
finite-dimensional vector space E with a norm, and a copy E' of this type with another norm,
then the identities from E to E' and from E'to E are continuous thanks to
LinearMap.continuous_of_finiteDimensional. This gives the desired norm equivalence.
A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.
Equations
- li.toLinearIsometryEquiv h = { toLinearEquiv := li.linearEquivOfInjective β― h, norm_map' := β― }
Instances For
An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.
Equations
- li.toAffineIsometryEquiv h = AffineIsometryEquiv.mk' (βli) (li.linearIsometry.toLinearIsometryEquiv h) default β―
Instances For
Reinterpret an affine equivalence as a homeomorphism.
Equations
- f.toHomeomorphOfFiniteDimensional = { toEquiv := f.toEquiv, continuous_toFun := β―, continuous_invFun := β― }
Instances For
Any K-Lipschitz map from a subset s of a metric space Ξ± to a finite-dimensional real
vector space E' can be extended to a Lipschitz map on the whole space Ξ±, with a slightly worse
constant C * K where C only depends on E'. We record a working value for this constant C
as lipschitzExtensionConstant E'.
Equations
- lipschitzExtensionConstant E' = let A := (Basis.ofVectorSpace β E').equivFun.toContinuousLinearEquiv; ββA.symmββ * ββAββ β 1
Instances For
Any K-Lipschitz map from a subset s of a metric space Ξ± to a finite-dimensional real
vector space E' can be extended to a Lipschitz map on the whole space Ξ±, with a slightly worse
constant lipschitzExtensionConstant E' * K.
A LinearMap on a finite-dimensional space over a complete field
is injective iff it is anti-Lipschitz.
The set of injective continuous linear maps E β F is open,
if E is finite-dimensional over a complete field.
Alias of Basis.opNNNorm_le.
Alias of Basis.opNorm_le.
A weaker version of Basis.opNNNorm_le that abstracts away the value of C.
Alias of Basis.exists_opNNNorm_le.
A weaker version of Basis.opNNNorm_le that abstracts away the value of C.
A weaker version of Basis.opNorm_le that abstracts away the value of C.
Alias of Basis.exists_opNorm_le.
A weaker version of Basis.opNorm_le that abstracts away the value of C.
In an infinite dimensional space, given a finite number of points, one may find a point
with norm at most R which is at distance at least 1 of all these points.
In an infinite-dimensional normed space, there exists a sequence of points which are all
bounded by R and at distance at least 1. For a version not assuming c and R, see
exists_seq_norm_le_one_le_norm_sub.
Riesz's theorem: if a closed ball with center zero of positive radius is compact in a vector space, then the space is finite-dimensional.
Alias of FiniteDimensional.of_isCompact_closedBallβ.
Riesz's theorem: if a closed ball with center zero of positive radius is compact in a vector space, then the space is finite-dimensional.
Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.
Alias of FiniteDimensional.of_isCompact_closedBall.
Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.
Riesz's theorem: a locally compact normed vector space is finite-dimensional.
Alias of FiniteDimensional.of_locallyCompactSpace.
Riesz's theorem: a locally compact normed vector space is finite-dimensional.
If a function has compact support, then either the function is trivial or the space is finite-dimensional.
If a function has compact multiplicative support, then either the function is trivial or the space is finite-dimensional.
A locally compact normed vector space is proper.
Continuous linear equivalence between continuous linear functions πβΏ β E and EβΏ.
The spaces πβΏ and EβΏ are represented as ΞΉ β π and ΞΉ β E, respectively,
where ΞΉ is a finite type.
Equations
- ContinuousLinearEquiv.piRing ΞΉ = { toLinearEquiv := LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing π E ΞΉ π), continuous_toFun := β―, continuous_invFun := β― }
Instances For
A family of continuous linear maps is continuous on s if all its applications are.
Any finite-dimensional vector space over a locally compact field is proper.
We do not register this as an instance to avoid an instance loop when trying to prove the
properness of π, and the search for π as an unknown metavariable. Declare the instance
explicitly when needed.
A submodule of a locally compact space over a complete field is also locally compact (and even proper).
If E is a finite dimensional normed real vector space, x : E, and s is a neighborhood of
x that is not equal to the whole space, then there exists a point y β frontier s at distance
Metric.infDist x sαΆ from x. See also
IsCompact.exists_mem_frontier_infDist_compl_eq_dist.
If K is a compact set in a nontrivial real normed space and x β K, then there exists a point
y of the boundary of K at distance Metric.infDist x KαΆ from x. See also
exists_mem_frontier_infDist_compl_eq_dist.
In a finite dimensional vector space over β, the series β x, βf xβ is unconditionally
summable if and only if the series β x, f x is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite dimensional spaces.
Alias of the reverse direction of summable_norm_iff.
In a finite dimensional vector space over β, the series β x, βf xβ is unconditionally
summable if and only if the series β x, f x is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite dimensional spaces.