# mathlibdocumentation

analysis.normed_space.finite_dimension

# 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 closed
• finite_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 register finite_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.

noncomputable def linear_isometry.to_linear_isometry_equiv {F : Type u_2} {Eβ : Type u_3} [normed_add_comm_group Eβ] {Rβ : Type u_4} [field Rβ] [module Rβ Eβ] [module Rβ F] [ Eβ] [ F] (li : Eβ ββα΅’[Rβ] F) (h : Eβ = ) :
Eβ ββα΅’[Rβ] F

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

Equations
@[simp]
theorem linear_isometry.coe_to_linear_isometry_equiv {F : Type u_2} {Eβ : Type u_3} [normed_add_comm_group Eβ] {Rβ : Type u_4} [field Rβ] [module Rβ Eβ] [module Rβ F] [ Eβ] [ F] (li : Eβ ββα΅’[Rβ] F) (h : Eβ = ) :
@[simp]
theorem linear_isometry.to_linear_isometry_equiv_apply {F : Type u_2} {Eβ : Type u_3} [normed_add_comm_group Eβ] {Rβ : Type u_4} [field Rβ] [module Rβ Eβ] [module Rβ F] [ Eβ] [ F] (li : Eβ ββα΅’[Rβ] F) (h : Eβ = ) (x : Eβ) :
noncomputable def affine_isometry.to_affine_isometry_equiv {π : Type u_1} {Vβ : Type u_2} {Vβ : Type u_3} {Pβ : Type u_4} {Pβ : Type u_5} [normed_field π] [normed_add_comm_group Vβ] [normed_space π Vβ] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] [ Vβ] [ Vβ] [inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : Vβ = Vβ) :
Pβ βα΅β±[π] Pβ

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

Equations
@[simp]
theorem affine_isometry.coe_to_affine_isometry_equiv {π : Type u_1} {Vβ : Type u_2} {Vβ : Type u_3} {Pβ : Type u_4} {Pβ : Type u_5} [normed_field π] [normed_add_comm_group Vβ] [normed_space π Vβ] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] [ Vβ] [ Vβ] [inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : Vβ = Vβ) :
@[simp]
theorem affine_isometry.to_affine_isometry_equiv_apply {π : Type u_1} {Vβ : Type u_2} {Vβ : Type u_3} {Pβ : Type u_4} {Pβ : Type u_5} [normed_field π] [normed_add_comm_group Vβ] [normed_space π Vβ] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] [ Vβ] [ Vβ] [inhabited Pβ] (li : Pβ βα΅β±[π] Pβ) (h : Vβ = Vβ) (x : Pβ) :
theorem affine_map.continuous_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE βα΅[π] PF) :
theorem affine_equiv.continuous_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE βα΅[π] PF) :
def affine_equiv.to_homeomorph_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE βα΅[π] PF) :

Reinterpret an affine equivalence as a homeomorphism.

Equations
@[simp]
theorem affine_equiv.coe_to_homeomorph_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE βα΅[π] PF) :
@[simp]
theorem affine_equiv.coe_to_homeomorph_of_finite_dimensional_symm {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE βα΅[π] PF) :
theorem continuous_linear_map.continuous_det {π : Type u} {E : Type v} [normed_space π E] [complete_space π] :
continuous (Ξ» (f : E βL[π] E), f.det)
@[irreducible]
noncomputable def lipschitz_extension_constant (E' : Type u_1) [ E']  :

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
theorem lipschitz_extension_constant_pos (E' : Type u_1) [ E']  :
theorem lipschitz_on_with.extend_finite_dimension {Ξ± : Type u_1} {E' : Type u_2} [ E'] {s : set Ξ±} {f : Ξ± β E'} {K : nnreal} (hf : s) :
β (g : Ξ± β E'), β§ 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 lipschitz_extension_constant E' * K.

theorem linear_map.exists_antilipschitz_with {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ E] (f : E ββ[π] F) (hf : = β₯) :
β (K : nnreal) (H : K > 0),
@[protected]
theorem linear_independent.eventually {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {ΞΉ : Type u_1} [finite ΞΉ] {f : ΞΉ β E} (hf : f) :
βαΆ  (g : ΞΉ β E) in nhds f, g
theorem is_open_set_of_linear_independent {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {ΞΉ : Type u_1} [finite ΞΉ] :
is_open {f : ΞΉ β E | f}
theorem is_open_set_of_nat_le_rank {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] (n : β) :
is_open {f : E βL[π] F | βn β€ rank βf}
theorem finite_dimensional.nonempty_continuous_linear_equiv_of_finrank_eq {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ E] [ F] (cond : = ) :
nonempty (E βL[π] F)

Two finite-dimensional normed spaces are continuously linearly equivalent if they have the same (finite) dimension.

theorem finite_dimensional.nonempty_continuous_linear_equiv_iff_finrank_eq {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ E] [ F] :
nonempty (E βL[π] F) β =

Two finite-dimensional normed spaces are continuously linearly equivalent if and only if they have the same (finite) dimension.

noncomputable def continuous_linear_equiv.of_finrank_eq {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ E] [ F] (cond : = ) :
E βL[π] F

A continuous linear equivalence between two finite-dimensional normed spaces of the same (finite) dimension.

Equations
noncomputable def basis.constrL {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π E) (f : ΞΉ β F) :
E βL[π] F

Construct a continuous linear map given the value at a finite basis.

Equations
@[simp, norm_cast]
theorem basis.coe_constrL {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π E) (f : ΞΉ β F) :
β(v.constrL f) = β(v.constr π) f
noncomputable def basis.equiv_funL {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π E) :
E βL[π] ΞΉ β π

The continuous linear equivalence between a vector space over π with a finite basis and functions from its basis indexing type to π.

Equations
@[simp]
theorem basis.constrL_apply {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π E) (f : ΞΉ β F) (e : E) :
β(v.constrL f) e = finset.univ.sum (Ξ» (i : ΞΉ), β(v.equiv_fun) e i β’ f i)
@[simp]
theorem basis.constrL_basis {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π E) (f : ΞΉ β F) (i : ΞΉ) :
β(v.constrL f) (βv i) = f i
theorem basis.op_nnnorm_le {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (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} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] (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} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [finite ΞΉ] (v : basis ΞΉ π E) :
β (C : nnreal) (H : 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} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {ΞΉ : Type u_1} [finite ΞΉ] (v : basis ΞΉ π E) :
β (C : β) (H : 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.

@[protected, instance]
def continuous_linear_map.topological_space.second_countable_topology {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ E]  :
theorem finite_dimensional.complete (π : Type u) (E : Type v) [normed_space π E] [complete_space π] [ E] :
theorem submodule.complete_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] [complete_space π] (s : submodule π E) [ β₯s] :

A finite-dimensional subspace is complete.

theorem submodule.closed_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] [complete_space π] (s : submodule π E) [ β₯s] :

A finite-dimensional subspace is closed.

theorem affine_subspace.closed_of_finite_dimensional {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {P : Type u_1} [metric_space P] [ P] (s : affine_subspace π P) [ β₯(s.direction)] :
theorem exists_norm_le_le_norm_sub_of_finset {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {c : π} (hc : 1 < β₯cβ₯) {R : β} (hR : β₯cβ₯ < R) (h : Β¬ E) (s : finset E) :
β (x : E), β§ β (y : 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} [normed_space π E] [complete_space π] {c : π} (hc : 1 < β₯cβ₯) {R : β} (hR : β₯cβ₯ < R) (h : Β¬ E) :
β (f : β β E), (β (n : β), β₯f nβ₯ β€ R) β§ β (m n : β), 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} [normed_space π E] [complete_space π] (h : Β¬ E) :
β (R : β) (f : β β E), 1 < R β§ (β (n : β), β₯f nβ₯ β€ R) β§ β (m n : β), m β  n β 1 β€ β₯f m - f nβ₯
theorem finite_dimensional_of_is_compact_closed_ballβ (π : Type u) {E : Type v} [normed_space π E] [complete_space π] {r : β} (rpos : 0 < r) (h : is_compact r)) :
E

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 finite_dimensional_of_is_compact_closed_ball (π : Type u) {E : Type v} [normed_space π E] [complete_space π] {r : β} (rpos : 0 < r) {c : E} (h : is_compact r)) :
E

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

theorem linear_equiv.closed_embedding_of_injective {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {f : E ββ[π] F} (hf : = β₯) [ E] :

An injective linear map with finite-dimensional domain is a closed embedding.

theorem continuous_linear_map.exists_right_inverse_of_surjective {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] [ F] (f : E βL[π] F) (hf : f.range = β€) :
β (g : F βL[π] E), f.comp g = F
theorem closed_embedding_smul_left {π : Type u} {E : Type v} [normed_space π E] [complete_space π] {c : E} (hc : c β  0) :
closed_embedding (Ξ» (x : π), x β’ c)
theorem is_closed_map_smul_left {π : Type u} {E : Type v} [normed_space π E] [complete_space π] (c : E) :
is_closed_map (Ξ» (x : π), x β’ c)
def continuous_linear_equiv.pi_ring {π : Type u} {E : Type v} [normed_space π E] [complete_space π] (ΞΉ : Type u_1) [fintype ΞΉ] [decidable_eq ΞΉ] :
((ΞΉ β π) β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
theorem continuous_on_clm_apply {π : Type u} {E : Type v} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {X : Type u_1} [ E] {f : X β (E βL[π] F)} {s : set X} :
β β (y : E), continuous_on (Ξ» (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} [normed_space π E] {F : Type w} [normed_space π F] [complete_space π] {X : Type u_1} [ E] {f : X β (E βL[π] F)} :
β β (y : E), continuous (Ξ» (x : X), β(f x) y)
theorem finite_dimensional.proper (π : Type u) (E : Type v) [normed_space π E] [proper_space π] [ E] :

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.

@[protected, instance]
def finite_dimensional.proper_real (E : Type u) [ E]  :
theorem exists_mem_frontier_inf_dist_compl_eq_dist {E : Type u_1} [ E] {x : E} {s : set E} (hx : x β s) (hs : s β  set.univ) :
β (y : E) (H : y β frontier s), =

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.

theorem is_compact.exists_mem_frontier_inf_dist_compl_eq_dist {E : Type u_1} [ E] [nontrivial E] {x : E} {K : set E} (hK : is_compact K) (hx : x β K) :
β (y : E) (H : y β frontier K), =

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.

theorem summable_norm_iff {Ξ± : Type u_1} {E : Type u_2} [ E] {f : Ξ± β E} :
summable (Ξ» (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_is_O' {ΞΉ : Type u_1} {E : Type u_2} {F : Type u_3} [ F] {f : ΞΉ β E} {g : ΞΉ β F} (hg : summable g) (h : f =O[filter.cofinite] g) :
theorem summable_of_is_O_nat' {E : Type u_1} {F : Type u_2} [ F] {f : β β E} {g : β β F} (hg : summable g) (h : f =O[filter.at_top] g) :
theorem summable_of_is_equivalent {ΞΉ : Type u_1} {E : Type u_2} [ E] {f g : ΞΉ β E} (hg : summable g)  :
theorem summable_of_is_equivalent_nat {E : Type u_1} [ E] {f g : β β E} (hg : summable g)  :
theorem is_equivalent.summable_iff {ΞΉ : Type u_1} {E : Type u_2} [ E] {f g : ΞΉ β E}  :
theorem is_equivalent.summable_iff_nat {E : Type u_1} [ E] {f g : β β E}  :