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 closedfinite_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 registerfinite_dimensional.completeonβorβ.
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
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)
with π^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
continuous, in linear_map.continuous_of_finite_dimensional.
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
Equations
- f.to_continuous_linear_map = {to_linear_map := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, cont := _}
The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.
Equations
- e.to_continuous_linear_equiv = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
A finite-dimensional subspace is complete.
A finite-dimensional subspace is closed.
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
properness of π, and the search for π as an unknown metavariable. Declare the instance
explicitly when needed.
Equations
- _ = _