# mathlibdocumentation

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 ℂ.
• 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.

def linear_isometry.to_linear_isometry_equiv {F : Type u_2} {E₁ : Type u_3} [normed_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [ E₁] [ F] (li : E₁ →ₗᵢ[R₁] F) (h : = ) :
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_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [ E₁] [ F] (li : E₁ →ₗᵢ[R₁] F) (h : = ) :
@[simp]
theorem linear_isometry.to_linear_isometry_equiv_apply {F : Type u_2} {E₁ : Type u_3} [normed_group E₁] {R₁ : Type u_4} [field R₁] [module R₁ E₁] [module R₁ F] [ E₁] [ F] (li : E₁ →ₗᵢ[R₁] F) (h : = ) (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₁] [ V₁] [ V₂] [metric_space P₁] [ P₁] [ P₂] [ V₁] [ V₂] [inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : = ) :
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₁] [ V₁] [ V₂] [metric_space P₁] [ P₁] [ P₂] [ V₁] [ V₂] [inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : = ) :
@[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₁] [ V₁] [ V₂] [metric_space P₁] [ P₁] [ P₂] [ V₁] [ V₂] [inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : = ) (x : P₁) :
theorem linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜] {E : Type v} [ E] [ E] (f : (ι → 𝕜) →ₗ[𝕜] E) :

A linear map on ι → 𝕜 (where ι is a fintype) is continuous

theorem continuous_equiv_fun_basis {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {ι : Type v} [fintype ι] (ξ : 𝕜 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} {E : Type v} [normed_group E] [ E] {F' : Type x} [add_comm_group F'] [ F'] [ F'] [ 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} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] {PE : Type u_1} {PF : Type u_2} [metric_space PE] [ PE] [metric_space PF] [ PF] [ E] (f : PE →ᵃ[𝕜] PF) :
def linear_map.to_continuous_linear_map {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F' : Type x} [add_comm_group F'] [ F'] [ F'] [ 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} {E : Type v} [normed_group E] [ E] {F' : Type x} [add_comm_group F'] [ F'] [ F'] [ E] (f : E →ₗ[𝕜] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F' : Type x} [add_comm_group F'] [ F'] [ F'] [ E] (f : E →ₗ[𝕜] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map_symm {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F' : Type x} [add_comm_group F'] [ F'] [ F'] [ E] :
def linear_equiv.to_continuous_linear_equiv {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] [ 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} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] [ E] (f : E →ₗ[𝕜] F) (hf : f.ker = ) :
∃ (K : ℝ≥0) (H : K > 0),
theorem linear_independent.eventually {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {ι : Type u_1} [fintype ι] {f : ι → E} (hf : f) :
∀ᶠ (g : ι → E) in 𝓝 f,
theorem is_open_set_of_linear_independent {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {ι : Type u_1} [fintype ι] :
is_open {f : ι → E |
theorem is_open_set_of_nat_le_rank {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] (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_group E] [ E] {F : Type w} [normed_group F] [ F] [ 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_group E] [ E] {F : Type w} [normed_group F] [ F] [ 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.

def continuous_linear_equiv.of_finrank_eq {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] [ E] [ F] (cond : = ) :
E ≃L[𝕜] F

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

Equations
def basis.constrL {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] {ι : Type u_1} [fintype ι] (v : 𝕜 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} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] {ι : Type u_1} [fintype ι] (v : 𝕜 E) (f : ι → F) :
(v.constrL f) = (v.constr 𝕜) f
def basis.equiv_funL {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {ι : Type u_1} [fintype ι] (v : 𝕜 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_group E] [ E] {F : Type w} [normed_group F] [ F] {ι : Type u_1} [fintype ι] (v : 𝕜 E) (f : ι → F) (e : E) :
(v.constrL f) e = ∑ (i : ι), (v.equiv_fun) e i f i
@[simp]
theorem basis.constrL_basis {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] {ι : Type u_1} [fintype ι] (v : 𝕜 E) (f : ι → F) (i : ι) :
(v.constrL f) (v i) = f i
theorem basis.sup_norm_le_norm {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {ι : Type u_1} [fintype ι] (v : 𝕜 E) :
∃ (C : ) (H : C > 0), ∀ (e : E), ∑ (i : ι), (v.equiv_fun) e i C * e
theorem basis.op_norm_le {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] {ι : Type u_1} [fintype ι] (v : 𝕜 E) :
∃ (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} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] [ E]  :
theorem finite_dimensional.complete (𝕜 : Type u) (E : Type v) [normed_group E] [ E] [ E] :
theorem submodule.complete_of_finite_dimensional {𝕜 : Type u} {E : Type v} [normed_group E] [ E] (s : E) [ s] :

A finite-dimensional subspace is complete.

theorem submodule.closed_of_finite_dimensional {𝕜 : Type u} {E : Type v} [normed_group E] [ E] (s : E) [ s] :

A finite-dimensional subspace is closed.

theorem exists_norm_le_le_norm_sub_of_finset {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {c : 𝕜} (hc : 1 < c) {R : } (hR : c < R) (h : ¬) (s : finset E) :
∃ (x : E), x R ∀ (y : E), y s1 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_group E] [ E] {c : 𝕜} (hc : 1 < c) {R : } (hR : c < R) (h : ¬) :
∃ (f : → E), (∀ (n : ), f n R) ∀ (m n : ), m n1 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_group E] [ E] (h : ¬) :
∃ (R : ) (f : → E), 1 < R (∀ (n : ), f n R) ∀ (m n : ), m n1 f m - f n
theorem finite_dimensional_of_is_compact_closed_ball (𝕜 : Type u) {E : Type v} [normed_group E] [ E] {r : } (rpos : 0 < r) (h : is_compact 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} {E : Type v} [normed_group E] [ E] {F : Type w} [normed_group F] [ F] [ F] (f : E →L[𝕜] F) (hf : f.range = ) :
∃ (g : F →L[𝕜] E), f.comp g =
theorem closed_embedding_smul_left {𝕜 : Type u} {E : Type v} [normed_group E] [ E] {c : E} (hc : c 0) :
closed_embedding (λ (x : 𝕜), x c)
theorem is_closed_map_smul_left {𝕜 : Type u} {E : Type v} [normed_group E] [ E] (c : E) :
is_closed_map (λ (x : 𝕜), x c)
theorem finite_dimensional.proper (𝕜 : Type u) (E : Type v) [normed_group E] [ 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.

@[instance]
def finite_dimensional.proper_real (E : Type u) [normed_group E] [ E]  :
theorem summable_norm_iff {α : Type u_1} {E : Type u_2} [normed_group E] [ 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} [normed_group E] [normed_group F] [ F] {f : ι → E} {g : ι → F} (hg : summable g) (h : filter.cofinite) :
theorem summable_of_is_O_nat' {E : Type u_1} {F : Type u_2} [normed_group E] [normed_group F] [ F] {f : → E} {g : → F} (hg : summable g) (h : filter.at_top) :
theorem summable_of_is_equivalent {ι : Type u_1} {E : Type u_2} [normed_group E] [ 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] [ 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] [ E] {f g : ι → E} (h : f ~[filter.cofinite] g) :
theorem is_equivalent.summable_iff_nat {E : Type u_1} [normed_group E] [ E] {f g : → E} (h : f ~[filter.at_top] g) :