mathlib documentation

analysis.normed_space.finite_dimension

Finite dimensional normed spaces over complete fields #

Over a complete nondiscrete 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: #

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.

def linear_isometry.to_linear_isometry_equiv {F : Type u_2} {E₁ : Type u_3} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
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} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) :
@[simp]
theorem linear_isometry.to_linear_isometry_equiv_apply {F : Type u_2} {E₁ : Type u_3} [semi_normed_group F] [normed_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [finite_dimensional R₁ E₁] [finite_dimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : finite_dimensional.finrank R₁ E₁ = finite_dimensional.finrank R₁ F) (x : E₁) :
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_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [finite_dimensional π•œ V₁] [finite_dimensional π•œ Vβ‚‚] [inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : finite_dimensional.finrank π•œ V₁ = finite_dimensional.finrank π•œ 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_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [finite_dimensional π•œ V₁] [finite_dimensional π•œ Vβ‚‚] [inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : finite_dimensional.finrank π•œ V₁ = finite_dimensional.finrank π•œ 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_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [finite_dimensional π•œ V₁] [finite_dimensional π•œ Vβ‚‚] [inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : finite_dimensional.finrank π•œ V₁ = finite_dimensional.finrank π•œ Vβ‚‚) (x : P₁) :
theorem linear_map.continuous_on_pi {ΞΉ : Type w} [fintype ΞΉ] {π•œ : Type u} [normed_field π•œ] {E : Type v} [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_smul π•œ E] (f : (ΞΉ β†’ π•œ) β†’β‚—[π•œ] E) :

A linear map on ΞΉ β†’ π•œ (where ΞΉ is a fintype) is continuous

theorem continuous_equiv_fun_basis {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type v} [fintype ΞΉ] (ΞΎ : basis ΞΉ π•œ E) :

In finite dimension over a complete field, the canonical identification (in terms of a basis) with π•œ^n together with its sup norm is continuous. This is the nontrivial part in the fact that all norms are equivalent in finite dimension.

This statement is superceded by the fact that every linear map on a finite-dimensional space is continuous, in linear_map.continuous_of_finite_dimensional.

theorem linear_map.continuous_of_finite_dimensional {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F' : Type x} [add_comm_group F'] [module π•œ F'] [topological_space F'] [topological_add_group F'] [has_continuous_smul π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F') :

Any linear map on a finite dimensional space over a complete field is continuous.

theorem affine_map.continuous_of_finite_dimensional {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [normed_add_torsor E PE] [metric_space PF] [normed_add_torsor F PF] [finite_dimensional π•œ E] (f : PE →ᡃ[π•œ] PF) :
def linear_map.to_continuous_linear_map {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F' : Type x} [add_comm_group F'] [module π•œ F'] [topological_space F'] [topological_add_group F'] [has_continuous_smul π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] :
(E β†’β‚—[π•œ] F') ≃ₗ[π•œ] E β†’L[π•œ] F'

The continuous linear map induced by a linear map on a finite dimensional space

Equations
@[simp]
theorem linear_map.coe_to_continuous_linear_map' {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F' : Type x} [add_comm_group F'] [module π•œ F'] [topological_space F'] [topological_add_group F'] [has_continuous_smul π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F' : Type x} [add_comm_group F'] [module π•œ F'] [topological_space F'] [topological_add_group F'] [has_continuous_smul π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map_symm {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F' : Type x} [add_comm_group F'] [module π•œ F'] [topological_space F'] [topological_add_group F'] [has_continuous_smul π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] :
def linear_equiv.to_continuous_linear_equiv {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
E ≃L[π•œ] F

The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.

Equations
theorem linear_map.exists_antilipschitz_with {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F) (hf : f.ker = βŠ₯) :
βˆƒ (K : ℝβ‰₯0) (H : K > 0), antilipschitz_with K ⇑f
theorem linear_independent.eventually {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] {f : ΞΉ β†’ E} (hf : linear_independent π•œ f) :
βˆ€αΆ  (g : ΞΉ β†’ E) in 𝓝 f, linear_independent π•œ g
theorem is_open_set_of_linear_independent {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] :
is_open {f : ΞΉ β†’ E | linear_independent π•œ f}
theorem is_open_set_of_nat_le_rank {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [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} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (cond : finite_dimensional.finrank π•œ E = finite_dimensional.finrank π•œ F) :
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} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] [finite_dimensional π•œ F] :

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

def continuous_linear_equiv.of_finrank_eq {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (cond : finite_dimensional.finrank π•œ E = finite_dimensional.finrank π•œ F) :
E ≃L[π•œ] F

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

Equations
def basis.constrL {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [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]
theorem basis.coe_constrL {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π•œ E) (f : ΞΉ β†’ F) :
↑(v.constrL f) = ⇑(v.constr π•œ) f
def basis.equiv_funL {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [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} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π•œ E) (f : ΞΉ β†’ F) (e : E) :
⇑(v.constrL f) e = βˆ‘ (i : ΞΉ), ⇑(v.equiv_fun) e i β€’ f i
@[simp]
theorem basis.constrL_basis {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π•œ E) (f : ΞΉ β†’ F) (i : ΞΉ) :
⇑(v.constrL f) (⇑v i) = f i
theorem basis.sup_norm_le_norm {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π•œ E) :
βˆƒ (C : ℝ) (H : C > 0), βˆ€ (e : E), βˆ‘ (i : ΞΉ), βˆ₯⇑(v.equiv_fun) e iβˆ₯ ≀ C * βˆ₯eβˆ₯
theorem basis.op_norm_le {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] (v : basis ΞΉ π•œ E) :
βˆƒ (C : ℝ) (H : C > 0), βˆ€ {u : E β†’L[π•œ] F} {M : ℝ}, 0 ≀ M β†’ (βˆ€ (i : ΞΉ), βˆ₯⇑u (⇑v i)βˆ₯ ≀ M) β†’ βˆ₯uβˆ₯ ≀ C * M
theorem finite_dimensional.complete (π•œ : Type u) [nondiscrete_normed_field π•œ] (E : Type v) [normed_group E] [normed_space π•œ E] [complete_space π•œ] [finite_dimensional π•œ E] :
theorem submodule.complete_of_finite_dimensional {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] (s : submodule π•œ E) [finite_dimensional π•œ β†₯s] :

A finite-dimensional subspace is complete.

theorem submodule.closed_of_finite_dimensional {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] (s : submodule π•œ E) [finite_dimensional π•œ β†₯s] :

A finite-dimensional subspace is closed.

theorem exists_norm_le_le_norm_sub_of_finset {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {c : π•œ} (hc : 1 < βˆ₯cβˆ₯) {R : ℝ} (hR : βˆ₯cβˆ₯ < R) (h : Β¬finite_dimensional π•œ E) (s : finset E) :
βˆƒ (x : E), βˆ₯xβˆ₯ ≀ R ∧ βˆ€ (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} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {c : π•œ} (hc : 1 < βˆ₯cβˆ₯) {R : ℝ} (hR : βˆ₯cβˆ₯ < R) (h : Β¬finite_dimensional π•œ 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} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] (h : Β¬finite_dimensional π•œ 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) [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {r : ℝ} (rpos : 0 < r) (h : is_compact (metric.closed_ball 0 r)) :

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

theorem continuous_linear_map.exists_right_inverse_of_surjective {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] {F : Type w} [normed_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ F] (f : E β†’L[π•œ] F) (hf : f.range = ⊀) :
βˆƒ (g : F β†’L[π•œ] E), f.comp g = continuous_linear_map.id π•œ F
theorem closed_embedding_smul_left {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {c : E} (hc : c β‰  0) :
closed_embedding (Ξ» (x : π•œ), x β€’ c)
theorem is_closed_map_smul_left {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] (c : E) :
is_closed_map (Ξ» (x : π•œ), x β€’ c)
theorem finite_dimensional.proper (π•œ : Type u) [nondiscrete_normed_field π•œ] (E : Type v) [normed_group E] [normed_space π•œ E] [proper_space π•œ] [finite_dimensional π•œ 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.

theorem summable_norm_iff {Ξ± : Type u_1} {E : Type u_2} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {f : Ξ± β†’ E} :
summable (Ξ» (x : Ξ±), βˆ₯f xβˆ₯) ↔ summable f

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} [normed_group E] [complete_space E] [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F] {f : ΞΉ β†’ E} {g : ΞΉ β†’ F} (hg : summable g) (h : asymptotics.is_O f g filter.cofinite) :
theorem summable_of_is_O_nat' {E : Type u_1} {F : Type u_2} [normed_group E] [complete_space E] [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F] {f : β„• β†’ E} {g : β„• β†’ F} (hg : summable g) (h : asymptotics.is_O f g filter.at_top) :
theorem summable_of_is_equivalent {ΞΉ : Type u_1} {E : Type u_2} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {f g : ΞΉ β†’ E} (hg : summable g) (h : f ~[filter.cofinite] g) :
theorem summable_of_is_equivalent_nat {E : Type u_1} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {f g : β„• β†’ E} (hg : summable g) (h : f ~[filter.at_top] g) :
theorem is_equivalent.summable_iff {ΞΉ : Type u_1} {E : Type u_2} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {f g : ΞΉ β†’ E} (h : f ~[filter.cofinite] g) :