Finite dimensional normed spaces over complete fields #
Over a complete nondiscrete 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: #
linear_map.continuous_of_finite_dimensional: a linear map on a finite-dimensional space over a complete field is continuous.
finite_dimensional.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_finite_dimensional: a finite-dimensional subspace over a complete field is closed
finite_dimensional.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 register
finite_dimensional_of_is_compact_closed_ball: 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' and from
E are continuous thanks to
linear_map.continuous_of_finite_dimensional. This gives the desired norm equivalence.
A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.
An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.
A linear map on
ι → 𝕜 (where
ι is a fintype) is continuous
In finite dimension over a complete field, the canonical identification (in terms of a basis)
𝕜^n together with its sup norm is continuous. This is the nontrivial part in the fact that
all norms are equivalent in finite dimension.
This statement is superceded by the fact that every linear map on a finite-dimensional space is
Any linear map on a finite dimensional space over a complete field is continuous.
The continuous linear map induced by a linear map on a finite dimensional space
The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.
Two finite-dimensional normed spaces are continuously linearly equivalent if they have the same (finite) dimension.
Two finite-dimensional normed spaces are continuously linearly equivalent if and only if they have the same (finite) dimension.
A continuous linear equivalence between two finite-dimensional normed spaces of the same (finite) dimension.
Construct a continuous linear map given the value at a finite basis.
The continuous linear equivalence between a vector space over
𝕜 with a finite basis and
functions from its basis indexing type to
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
R and at distance at least
1. For a version not assuming
Riesz's theorem: if the unit ball is compact in a vector space, then the space is finite-dimensional.
Any finite-dimensional vector space over a proper field is proper.
We do not register this as an instance to avoid an instance loop when trying to prove the
𝕜, and the search for
𝕜 as an unknown metavariable. Declare the instance
explicitly when needed.
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.