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: #
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.complete
onβ
orβ
.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
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 isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.
Equations
- li.to_linear_isometry_equiv h = {to_linear_equiv := li.to_linear_map.linear_equiv_of_injective _ h, norm_map' := _}
An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.
Equations
- li.to_affine_isometry_equiv h = affine_isometry_equiv.mk' βli (li.linear_isometry.to_linear_isometry_equiv h) (arbitrary Pβ) _
Reinterpret an affine equivalence as a homeomorphism.
Equations
- f.to_homeomorph_of_finite_dimensional = {to_equiv := f.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
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 lipschitz_extension_constant E'
.
Equations
- lipschitz_extension_constant E' = let A : E' βL[β] β₯(basis.of_vector_space_index β E') β β := (basis.of_vector_space β E').equiv_fun.to_continuous_linear_equiv in linear_order.max (β₯A.symm.to_continuous_linear_mapβ₯β * β₯A.to_continuous_linear_mapβ₯β) 1
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 lipschitz_extension_constant E' * K
.
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.
Equations
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 π
.
Equations
- v.equiv_funL = {to_linear_equiv := {to_fun := v.equiv_fun.to_fun, map_add' := _, map_smul' := _, inv_fun := v.equiv_fun.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
A weaker version of basis.op_nnnorm_le
that abstracts away the value of C
.
A weaker version of basis.op_norm_le
that abstracts away the value of C
.
A finite-dimensional subspace is complete.
A finite-dimensional subspace is closed.
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.
Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.
An injective linear map with finite-dimensional domain is a closed embedding.
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
- continuous_linear_equiv.pi_ring ΞΉ = {to_linear_equiv := {to_fun := (linear_map.to_continuous_linear_map.symm.trans (linear_equiv.pi_ring π E ΞΉ π)).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_map.to_continuous_linear_map.symm.trans (linear_equiv.pi_ring π E ΞΉ π)).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
A family of continuous linear maps is continuous on s
if all its applications are.
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.
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.inf_dist x sαΆ
from x
. See also
is_compact.exists_mem_frontier_inf_dist_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.inf_dist x KαΆ
from x
. See also
exists_mem_frontier_inf_dist_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.