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:

linear_map.continuous_of_finite_dimensional : a linear map on a finite-dimensional space over a complete field is continuous.
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 ℂ.

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) :

continuous ⇑f

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 𝕜 ξ) :

continuous ⇑(hξ.equiv_fun)

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') :

continuous ⇑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] (f : E →ₗ[𝕜] F') :

E →L[𝕜] F'

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

Equations

f.to_continuous_linear_map = {to_linear_map := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, cont := _}

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

e.to_continuous_linear_equiv = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

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} (hv : is_basis 𝕜 v) (f : ι → F) :

E →L[𝕜] F

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

Equations

hv.constrL f = {to_linear_map := hv.constr f, cont := _}

@[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} (hv : 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

hv.equiv_funL = {to_linear_equiv := {to_fun := hv.equiv_fun.to_fun, map_add' := _, map_smul' := _, inv_fun := hv.equiv_fun.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

@[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} (hv : is_basis 𝕜 v) :

∃ (C : ℝ) (H : C > 0), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ∥⇑u (v i)∥ ≤ M) → ∥u∥ ≤ C * M

@[instance]

def continuous_linear_map.topological_space.second_countable_topology {𝕜 : 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] [topological_space.second_countable_topology F] :

topological_space.second_countable_topology (E →L[𝕜] F)

theorem finite_dimensional.complete (𝕜 : Type u) [nondiscrete_normed_field 𝕜] (E : Type v) [normed_group E] [normed_space 𝕜 E] [complete_space 𝕜] [finite_dimensional 𝕜 E] :

complete_space 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] :

is_complete ↑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) (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.

@[instance]

def finite_dimensional.proper_real (E : Type u) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :