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.

theorem linear_map.continuous_on_pi {ΞΉ : Type w} [fintype ΞΉ] {π•œ : Type u} [normed_field π•œ] {E : Type v} [add_comm_group E] [vector_space π•œ E] [topological_space E] [topological_add_group E] [topological_vector_space π•œ 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 ΞΉ] (ΞΎ : ΞΉ β†’ E) (hΞΎ : is_basis π•œ ΞΎ) :

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'] [vector_space π•œ F'] [topological_space F'] [topological_add_group F'] [topological_vector_space π•œ F'] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F') :

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

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'] [vector_space π•œ F'] [topological_space F'] [topological_add_group F'] [topological_vector_space π•œ 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
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 ≃ₗ[π•œ] F) β†’ (E ≃L[π•œ] F)

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

Equations
def is_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 : ΞΉ β†’ E} :
is_basis π•œ v β†’ (ΞΉ β†’ F) β†’ (E β†’L[π•œ] F)

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

Equations
@[simp]
theorem is_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 : ΞΉ β†’ E} (hv : is_basis π•œ v) (f : ΞΉ β†’ F) :
↑(hv.constrL f) = hv.constr f

def is_basis.equiv_funL {π•œ : Type u} [nondiscrete_normed_field π•œ] {E : Type v} [normed_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [fintype ΞΉ] {v : ΞΉ β†’ E} :
is_basis π•œ v β†’ (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 is_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 : ΞΉ β†’ E} (hv : is_basis π•œ v) (f : ΞΉ β†’ F) (e : E) :
⇑(hv.constrL f) e = βˆ‘ (i : ΞΉ), ⇑(hv.equiv_fun) e i β€’ f i

@[simp]
theorem is_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 : ΞΉ β†’ E} (hv : is_basis π•œ v) (f : ΞΉ β†’ F) (i : ΞΉ) :
⇑(hv.constrL f) (v i) = f i

theorem is_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 : ΞΉ β†’ E} (hv : is_basis π•œ v) :
βˆƒ (C : ℝ) (H : C > 0), βˆ€ (e : E), βˆ‘ (i : ΞΉ), βˆ₯⇑(hv.equiv_fun) e iβˆ₯ ≀ C * βˆ₯eβˆ₯

theorem is_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 : ΞΉ β†’ E} :
is_basis π•œ v β†’ (βˆƒ (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 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) :
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} :
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.