# Documentation

Mathlib.Analysis.NormedSpace.FiniteDimension

# 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 closed
• FiniteDimensional.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 FiniteDimensional.complete on ℝ 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.

def LinearIsometry.toLinearIsometryEquiv {F : Type u_2} {E₁ : Type u_3} [] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [] [] (li : E₁ →ₗᵢ[R₁] F) (h : ) :
E₁ ≃ₗᵢ[R₁] F

A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.

Instances For
@[simp]
theorem LinearIsometry.coe_toLinearIsometryEquiv {F : Type u_2} {E₁ : Type u_3} [] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [] [] (li : E₁ →ₗᵢ[R₁] F) (h : ) :
= li
@[simp]
theorem LinearIsometry.toLinearIsometryEquiv_apply {F : Type u_2} {E₁ : Type u_3} [] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [] [] (li : E₁ →ₗᵢ[R₁] F) (h : ) (x : E₁) :
↑() x = li x
def AffineIsometry.toAffineIsometryEquiv {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [] [] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [] [] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [] [] [] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : ) :
P₁ ≃ᵃⁱ[𝕜] P₂

An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.

Instances For
@[simp]
theorem AffineIsometry.coe_toAffineIsometryEquiv {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [] [] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [] [] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [] [] [] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : ) :
= li
@[simp]
theorem AffineIsometry.toAffineIsometryEquiv_apply {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [] [] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [] [] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [] [] [] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : ) (x : P₁) :
↑() x = li x
theorem AffineMap.continuous_of_finiteDimensional {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [] (f : PE →ᵃ[𝕜] PF) :
theorem AffineEquiv.continuous_of_finiteDimensional {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [] (f : PE ≃ᵃ[𝕜] PF) :
def AffineEquiv.toHomeomorphOfFiniteDimensional {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [] (f : PE ≃ᵃ[𝕜] PF) :
PE ≃ₜ PF

Reinterpret an affine equivalence as a homeomorphism.

Instances For
@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [] (f : PE ≃ᵃ[𝕜] PF) :
@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [] (f : PE ≃ᵃ[𝕜] PF) :
theorem ContinuousLinearMap.continuous_det {𝕜 : Type u} {E : Type v} [] [] :
Continuous fun f =>
@[irreducible]
def lipschitzExtensionConstant (E' : Type u_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 C * K where C only depends on E'. We record a working value for this constant C as lipschitzExtensionConstant E'.

Instances For
theorem lipschitzExtensionConstant_def (E' : Type u_1) [] [] [] :
= let A := ; max () 1
theorem lipschitzExtensionConstant_pos (E' : Type u_1) [] [] [] :
theorem LipschitzOnWith.extend_finite_dimension {α : Type u_1} {E' : Type u_2} [] [] [] {s : Set α} {f : αE'} {K : NNReal} (hf : ) :
g, Set.EqOn f g s

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.

theorem LinearMap.exists_antilipschitzWith {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] [] (f : E →ₗ[𝕜] F) (hf : ) :
K, K > 0
theorem LinearIndependent.eventually {𝕜 : Type u} {E : Type v} [] [] {ι : Type u_1} [] {f : ιE} (hf : ) :
∀ᶠ (g : ιE) in nhds f,
theorem isOpen_setOf_linearIndependent {𝕜 : Type u} {E : Type v} [] [] {ι : Type u_1} [] :
IsOpen {f | }
theorem isOpen_setOf_nat_le_rank {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] (n : ) :
IsOpen {f | n }
theorem Basis.op_nnnorm_le {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {ι : Type u_1} [] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : NNReal) (hu : ∀ (i : ι), u (v i)‖₊ M) :
theorem Basis.op_norm_le {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {ι : Type u_1} [] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : } (hM : 0 M) (hu : ∀ (i : ι), u (v i) M) :
theorem Basis.exists_op_nnnorm_le {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {ι : Type u_1} [] (v : Basis ι 𝕜 E) :
C, C > 0 ∀ {u : E →L[𝕜] F} (M : NNReal), (∀ (i : ι), u (v i)‖₊ M) → u‖₊ C * M

A weaker version of Basis.op_nnnorm_le that abstracts away the value of C.

theorem Basis.exists_op_norm_le {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {ι : Type u_1} [] (v : Basis ι 𝕜 E) :
C, C > 0 ∀ {u : E →L[𝕜] F} {M : }, 0 M(∀ (i : ι), u (v i) M) → u C * M

A weaker version of Basis.op_norm_le that abstracts away the value of C.

theorem AffineSubspace.closed_of_finiteDimensional {𝕜 : Type u} {E : Type v} [] [] {P : Type u_1} [] [] (s : ) [FiniteDimensional 𝕜 { x // }] :
theorem exists_norm_le_le_norm_sub_of_finset {𝕜 : Type u} {E : Type v} [] [] {c : 𝕜} (hc : 1 < c) {R : } (hR : c < R) (h : ) (s : ) :
x, x R ∀ (y : E), y s1 y - x

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.

theorem exists_seq_norm_le_one_le_norm_sub' {𝕜 : Type u} {E : Type v} [] [] {c : 𝕜} (hc : 1 < c) {R : } (hR : c < R) (h : ) :
f, (∀ (n : ), f n R) ∀ (m n : ), m n1 f m - f n

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.

theorem exists_seq_norm_le_one_le_norm_sub {𝕜 : Type u} {E : Type v} [] [] (h : ) :
R f, 1 < R (∀ (n : ), f n R) ∀ (m n : ), m n1 f m - f n
theorem finiteDimensional_of_isCompact_closedBall₀ (𝕜 : Type u) {E : Type v} [] [] {r : } (rpos : 0 < r) (h : ) :

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.

theorem finiteDimensional_of_isCompact_closedBall (𝕜 : Type u) {E : Type v} [] [] {r : } (rpos : 0 < r) {c : E} (h : ) :

Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.

theorem finiteDimensional_of_locallyCompactSpace (𝕜 : Type u) {E : Type v} [] [] :

Riesz's theorem: a locally compact normed vector space is finite-dimensional.

theorem HasCompactSupport.eq_zero_or_finiteDimensional (𝕜 : Type u) {E : Type v} [] [] {X : Type u_1} [] [Zero X] [] {f : EX} (hf : ) (h'f : ) :
f = 0

If a function has compact support, then either the function is trivial or the space is finite-dimensional.

theorem HasCompactMulSupport.eq_one_or_finiteDimensional (𝕜 : Type u) {E : Type v} [] [] {X : Type u_1} [] [One X] [] {f : EX} (hf : ) (h'f : ) :
f = 1

If a function has compact multiplicative support, then either the function is trivial or the space is finite-dimensional.

theorem properSpace_of_locallyCompactSpace (𝕜 : Type u_1) {E : Type u_2} [] :

A locally compact normed vector space is proper.

def ContinuousLinearEquiv.piRing {𝕜 : Type u} {E : Type v} [] [] (ι : Type u_1) [] [] :
((ι𝕜) →L[𝕜] E) ≃L[𝕜] ιE

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.

Instances For
theorem continuousOn_clm_apply {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {X : Type u_1} [] [] {f : XE →L[𝕜] F} {s : Set X} :
∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s

A family of continuous linear maps is continuous on s if all its applications are.

theorem continuous_clm_apply {𝕜 : Type u} {E : Type v} [] {F : Type w} [] [] {X : Type u_1} [] [] {f : XE →L[𝕜] F} :
∀ (y : E), Continuous fun x => ↑(f x) y
theorem FiniteDimensional.proper (𝕜 : Type u) (E : Type v) [] [] [] :

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.

instance FiniteDimensional.proper_real (E : Type u) [] [] :
theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [] [] {x : E} {s : Set E} (hx : x s) (hs : s Set.univ) :
y, y = dist x y

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.

theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [] [] {x : E} {K : Set E} (hK : ) (hx : x K) :
y, y = dist x y

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.

theorem summable_norm_iff {α : Type u_1} {E : Type u_2} [] [] {f : αE} :
(Summable fun x => f x)

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.

theorem summable_of_isBigO' {ι : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {f : ιE} {g : ιF} (hg : ) (h : f =O[Filter.cofinite] g) :
theorem summable_of_isBigO_nat' {E : Type u_1} {F : Type u_2} [] [] [] {f : E} {g : F} (hg : ) (h : f =O[Filter.atTop] g) :
theorem summable_of_isEquivalent {ι : Type u_1} {E : Type u_2} [] [] {f : ιE} {g : ιE} (hg : ) (h : Asymptotics.IsEquivalent Filter.cofinite f g) :
theorem summable_of_isEquivalent_nat {E : Type u_1} [] [] {f : E} {g : E} (hg : ) (h : Asymptotics.IsEquivalent Filter.atTop f g) :
theorem IsEquivalent.summable_iff {ι : Type u_1} {E : Type u_2} [] [] {f : ιE} {g : ιE} (h : Asymptotics.IsEquivalent Filter.cofinite f g) :
theorem IsEquivalent.summable_iff_nat {E : Type u_1} [] [] {f : E} {g : E} (h : Asymptotics.IsEquivalent Filter.atTop f g) :