# 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] [FiniteDimensional Rβ Eβ] [FiniteDimensional Rβ F] (li : Eβ ββα΅’[Rβ] F) (h : FiniteDimensional.finrank Rβ Eβ = ) :
Eβ ββα΅’[Rβ] F

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

Equations
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] [FiniteDimensional Rβ Eβ] [FiniteDimensional Rβ F] (li : Eβ ββα΅’[Rβ] F) (h : FiniteDimensional.finrank Rβ Eβ = ) :
β = β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] [FiniteDimensional Rβ Eβ] [FiniteDimensional Rβ F] (li : Eβ ββα΅’[Rβ] F) (h : FiniteDimensional.finrank Rβ Eβ = ) (x : Eβ) :
= li x
def AffineIsometry.toAffineIsometryEquiv {π : Type u_1} {Vβ : Type u_2} {Vβ : Type u_3} {Pβ : Type u_4} {Pβ : Type u_5} [NormedField π] [] [] [NormedSpace π Vβ] [NormedSpace π Vβ] [MetricSpace Pβ] [] [NormedAddTorsor Vβ Pβ] [NormedAddTorsor Vβ Pβ] [FiniteDimensional π Vβ] [FiniteDimensional π Vβ] [Inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : FiniteDimensional.finrank π Vβ = FiniteDimensional.finrank π Vβ) :
Pβ βα΅β±[π] Pβ

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

Equations
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} [NormedField π] [] [] [NormedSpace π Vβ] [NormedSpace π Vβ] [MetricSpace Pβ] [] [NormedAddTorsor Vβ Pβ] [NormedAddTorsor Vβ Pβ] [FiniteDimensional π Vβ] [FiniteDimensional π Vβ] [Inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : FiniteDimensional.finrank π Vβ = FiniteDimensional.finrank π Vβ) :
β = β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} [NormedField π] [] [] [NormedSpace π Vβ] [NormedSpace π Vβ] [MetricSpace Pβ] [] [NormedAddTorsor Vβ Pβ] [NormedAddTorsor Vβ Pβ] [FiniteDimensional π Vβ] [FiniteDimensional π Vβ] [Inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : FiniteDimensional.finrank π Vβ = FiniteDimensional.finrank π Vβ) (x : Pβ) :
= li x
theorem AffineMap.continuous_of_finiteDimensional {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [FiniteDimensional π E] (f : PE βα΅[π] PF) :
Continuous βf
theorem AffineEquiv.continuous_of_finiteDimensional {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [FiniteDimensional π E] (f : PE βα΅[π] PF) :
Continuous βf
def AffineEquiv.toHomeomorphOfFiniteDimensional {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [FiniteDimensional π E] (f : PE βα΅[π] PF) :

Reinterpret an affine equivalence as a homeomorphism.

Equations
• = { toEquiv := f.toEquiv, continuous_toFun := β―, continuous_invFun := β― }
Instances For
@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [FiniteDimensional π E] (f : PE βα΅[π] PF) :
= βf
@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {PE : Type u_1} {PF : Type u_2} [] [] [] [] [FiniteDimensional π E] (f : PE βα΅[π] PF) :
theorem ContinuousLinearMap.continuous_det {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] :
Continuous fun (f : E βL[π] E) =>
theorem lipschitzExtensionConstant_def (E' : Type u_1) [] [] [] :
= let A := ; max () 1
@[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'.

Equations
Instances For
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 : Ξ± β E'), β§ 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} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] [FiniteDimensional π E] (f : E ββ[π] F) (hf : ) :
β K > 0, AntilipschitzWith K βf
theorem LinearMap.injective_iff_antilipschitz {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] [FiniteDimensional π E] (f : E ββ[π] F) :
β β K > 0, AntilipschitzWith K βf

A LinearMap on a finite-dimensional space over a complete field is injective iff it is anti-Lipschitz.

theorem ContinuousLinearMap.isOpen_injective {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] [FiniteDimensional π E] :
IsOpen {L : E βL[π] F | }

The set of injective continuous linear maps E β F is open, if E is finite-dimensional over a complete field.

theorem LinearIndependent.eventually {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] {f : ΞΉ β E} (hf : LinearIndependent π f) :
βαΆ  (g : ΞΉ β E) in nhds f, LinearIndependent π g
theorem isOpen_setOf_linearIndependent {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] :
IsOpen {f : ΞΉ β E | LinearIndependent π f}
theorem isOpen_setOf_nat_le_rank {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] (n : β) :
IsOpen {f : E βL[π] F | βn β€ LinearMap.rank βf}
theorem Basis.opNNNorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π E) {u : E βL[π] F} (M : NNReal) (hu : β (i : ΞΉ), βu (v i)ββ β€ M) :
@[deprecated Basis.opNNNorm_le]
theorem Basis.op_nnnorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π E) {u : E βL[π] F} (M : NNReal) (hu : β (i : ΞΉ), βu (v i)ββ β€ M) :

Alias of Basis.opNNNorm_le.

theorem Basis.opNorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π E) {u : E βL[π] F} {M : β} (hM : 0 β€ M) (hu : β (i : ΞΉ), βu (v i)β β€ M) :
@[deprecated Basis.opNorm_le]
theorem Basis.op_norm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π E) {u : E βL[π] F} {M : β} (hM : 0 β€ M) (hu : β (i : ΞΉ), βu (v i)β β€ M) :

Alias of Basis.opNorm_le.

theorem Basis.exists_opNNNorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π E) :
β C > 0, β {u : E βL[π] F} (M : NNReal), (β (i : ΞΉ), βu (v i)ββ β€ M) β β€ C * M

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

@[deprecated Basis.exists_opNNNorm_le]
theorem Basis.exists_op_nnnorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π E) :
β C > 0, β {u : E βL[π] F} (M : NNReal), (β (i : ΞΉ), βu (v i)ββ β€ M) β β€ C * M

Alias of Basis.exists_opNNNorm_le.

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

theorem Basis.exists_opNorm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π E) :
β C > 0, β {u : E βL[π] F} {M : β}, 0 β€ M β (β (i : ΞΉ), βu (v i)β β€ M) β β€ C * M

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

@[deprecated Basis.exists_opNorm_le]
theorem Basis.exists_op_norm_le {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π E) :
β C > 0, β {u : E βL[π] F} {M : β}, 0 β€ M β (β (i : ΞΉ), βu (v i)β β€ M) β β€ C * M

Alias of Basis.exists_opNorm_le.

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

theorem AffineSubspace.closed_of_finiteDimensional {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {P : Type u_1} [] [] (s : AffineSubspace π P) [FiniteDimensional π β₯] :
IsClosed βs
theorem exists_norm_le_le_norm_sub_of_finset {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {c : π} (hc : 1 < ) {R : β} (hR : < R) (h : Β¬FiniteDimensional π E) (s : ) :
β (x : E), β§ β y β s, 1 β€ β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} [NormedSpace π E] [CompleteSpace π] {c : π} (hc : 1 < ) {R : β} (hR : < R) (h : Β¬FiniteDimensional π E) :
β (f : β β E), (β (n : β), βf nβ β€ R) β§ Pairwise fun (m n : β) => 1 β€ β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} [NormedSpace π E] [CompleteSpace π] (h : Β¬FiniteDimensional π E) :
β (R : β) (f : β β E), 1 < R β§ (β (n : β), βf nβ β€ R) β§ Pairwise fun (m n : β) => 1 β€ βf m - f nβ
theorem FiniteDimensional.of_isCompact_closedBallβ (π : Type u) [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {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.

@[deprecated FiniteDimensional.of_isCompact_closedBallβ]
theorem finiteDimensional_of_isCompact_closedBallβ (π : Type u) [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {r : β} (rpos : 0 < r) (h : ) :

Alias of FiniteDimensional.of_isCompact_closedBallβ.

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} [NormedSpace π E] [CompleteSpace π] {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.

@[deprecated FiniteDimensional.of_isCompact_closedBall]
theorem finiteDimensional_of_isCompact_closedBall (π : Type u) [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {r : β} (rpos : 0 < r) {c : E} (h : ) :

Alias of FiniteDimensional.of_isCompact_closedBall.

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} [NormedSpace π E] [CompleteSpace π] :

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

@[deprecated FiniteDimensional.of_locallyCompactSpace]
theorem finiteDimensional_of_locallyCompactSpace (π : Type u) [] {E : Type v} [NormedSpace π E] [CompleteSpace π] :

Alias of FiniteDimensional.of_locallyCompactSpace.

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

theorem HasCompactSupport.eq_zero_or_finiteDimensional (π : Type u) [] {E : Type v} [NormedSpace π E] [CompleteSpace π] {X : Type u_1} [] [Zero X] [] {f : E β X} (hf : ) (h'f : ) :
f = 0 β¨ FiniteDimensional π E

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} [NormedSpace π E] [CompleteSpace π] {X : Type u_1} [] [One X] [] {f : E β X} (hf : ) (h'f : ) :
f = 1 β¨ FiniteDimensional π E

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} [NormedSpace π E] :

A locally compact normed vector space is proper.

@[deprecated ProperSpace.of_locallyCompactSpace]
theorem properSpace_of_locallyCompactSpace (π : Type u_1) [] {E : Type u_2} [NormedSpace π E] :

Alias of ProperSpace.of_locallyCompactSpace.

A locally compact normed vector space is proper.

theorem ProperSpace.of_locallyCompact_module (π : Type u) [] (E : Type v) [NormedSpace π E] [CompleteSpace π] [] :
ProperSpace π
@[deprecated ProperSpace.of_locallyCompact_module]
theorem properSpace_of_locallyCompact_module (π : Type u) [] (E : Type v) [NormedSpace π E] [CompleteSpace π] [] :
ProperSpace π

Alias of ProperSpace.of_locallyCompact_module.

def ContinuousLinearEquiv.piRing {π : Type u} [] {E : Type v} [NormedSpace π E] [CompleteSpace π] (ΞΉ : Type u_1) [Fintype ΞΉ] [] :
((ΞΉ β π) β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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem continuousOn_clm_apply {π : Type u} [] {E : Type v} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {X : Type u_1} [] [FiniteDimensional π E] {f : X β E βL[π] F} {s : Set X} :
β β (y : E), ContinuousOn (fun (x : 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} [NormedSpace π E] {F : Type w} [NormedSpace π F] [CompleteSpace π] {X : Type u_1} [] [FiniteDimensional π E] {f : X β E βL[π] F} :
β β (y : E), Continuous fun (x : X) => (f x) y
theorem FiniteDimensional.proper (π : Type u) [] (E : Type v) [NormedSpace π E] [] [FiniteDimensional π E] :

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.

instance FiniteDimensional.proper_real (E : Type u) [] [] :
Equations
• β― = β―

A submodule of a locally compact space over a complete field is also locally compact (and even proper).

Equations
• β― = β―
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 β , = 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 β , = 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.norm {Ξ± : Type u_1} {E : Type u_2} [] [] {f : Ξ± β E} :
β Summable fun (x : Ξ±) => βf xβ

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.

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 Asymptotics.IsBigO.comp_summable {ΞΉ : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {f : E β F} (hf : f =O[nhds 0] id) {g : ΞΉ β E} (hg : ) :
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) :