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
An affine map from a finite-dimensional space is automatically Lipschitz.
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' = have A := (Module.Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; max (‖↑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.
An injective affine map from a finite-dimensional space is automatically anti-Lipschitz.
The set of injective continuous linear maps E → F is open,
if E is finite-dimensional over a complete field.
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.
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.
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.
If the identity operator of a Banach space over a nontrivially normed field is compact, then the space is finite dimensional.
Alias of FiniteDimensional.of_isCompactOperator_id.
If the identity operator of a Banach space over a nontrivially normed field is compact, then the space is finite dimensional.
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.
This is a version of summable_norm_mul_geometric_of_norm_lt_one for more general codomains. We
keep the original one due to import restrictions.
Alias of Asymptotics.IsEquivalent.summable_iff.