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