mathlib documentation

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

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} [seminormed_add_comm_group F] [normed_add_comm_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} [seminormed_add_comm_group F] [normed_add_comm_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} [seminormed_add_comm_group F] [normed_add_comm_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₁) :
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₁] [seminormed_add_comm_group Vβ‚‚] [normed_space π•œ V₁] [normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [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_add_comm_group V₁] [seminormed_add_comm_group Vβ‚‚] [normed_space π•œ V₁] [normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [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_add_comm_group V₁] [seminormed_add_comm_group Vβ‚‚] [normed_space π•œ V₁] [normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [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 affine_map.continuous_of_finite_dimensional {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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) :
theorem affine_equiv.continuous_of_finite_dimensional {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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 affine_equiv.to_homeomorph_of_finite_dimensional {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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) :

Reinterpret an affine equivalence as a homeomorphism.

Equations
theorem continuous_linear_map.continuous_det {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] :
continuous (Ξ» (f : E β†’L[π•œ] E), f.det)
@[irreducible]

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

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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ E] (f : E β†’β‚—[π•œ] F) (hf : linear_map.ker f = βŠ₯) :
@[protected]
theorem linear_independent.eventually {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [finite ΞΉ] {f : ΞΉ β†’ E} (hf : linear_independent π•œ f) :
βˆ€αΆ  (g : ΞΉ β†’ E) in nhds f, linear_independent π•œ g
theorem is_open_set_of_linear_independent {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {ΞΉ : Type u_1} [finite ΞΉ] :
is_open {f : ΞΉ β†’ E | linear_independent π•œ f}
theorem is_open_set_of_nat_le_rank {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] (n : β„•) :
is_open {f : E β†’L[π•œ] F | ↑n ≀ rank ↑f}

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

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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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
noncomputable def basis.constrL {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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, norm_cast]
theorem basis.coe_constrL {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_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.op_nnnorm_le {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [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.

theorem finite_dimensional.complete (π•œ : Type u) [nontrivially_normed_field π•œ] (E : Type v) [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] [finite_dimensional π•œ E] :
theorem submodule.complete_of_finite_dimensional {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {c : π•œ} (hc : 1 < β€–cβ€–) {R : ℝ} (hR : β€–cβ€– < R) (h : Β¬finite_dimensional π•œ E) (s : finset E) :

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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {c : π•œ} (hc : 1 < β€–cβ€–) {R : ℝ} (hR : β€–cβ€– < R) (h : Β¬finite_dimensional π•œ E) :

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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] (h : Β¬finite_dimensional π•œ E) :
theorem finite_dimensional_of_is_compact_closed_ballβ‚€ (π•œ : Type u) [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {r : ℝ} (rpos : 0 < r) (h : is_compact (metric.closed_ball 0 r)) :

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) [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {r : ℝ} (rpos : 0 < r) {c : E} (h : is_compact (metric.closed_ball c r)) :

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

theorem has_compact_support.eq_zero_or_finite_dimensional (π•œ : Type u) [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {X : Type u_1} [topological_space X] [has_zero X] [t2_space X] {f : E β†’ X} (hf : has_compact_support f) (h'f : continuous f) :
f = 0 ∨ finite_dimensional π•œ E

If a function has compact support, then either the function is trivial or the space if finite-dimensional.

theorem has_compact_mul_support.eq_one_or_finite_dimensional (π•œ : Type u) [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] {X : Type u_1} [topological_space X] [has_one X] [t2_space X] {f : E β†’ X} (hf : has_compact_mul_support f) (h'f : continuous f) :
f = 1 ∨ finite_dimensional π•œ E

If a function has compact multiplicative support, then either the function is trivial or the space if finite-dimensional.

theorem linear_equiv.closed_embedding_of_injective {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] {f : E β†’β‚—[π•œ] F} (hf : linear_map.ker f = βŠ₯) [finite_dimensional π•œ E] :

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

theorem continuous_linear_map.exists_right_inverse_of_surjective {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] [finite_dimensional π•œ F] (f : E β†’L[π•œ] F) (hf : linear_map.range f = ⊀) :
βˆƒ (g : F β†’L[π•œ] E), f.comp g = continuous_linear_map.id π•œ F
theorem closed_embedding_smul_left {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] [complete_space π•œ] (c : E) :
is_closed_map (Ξ» (x : π•œ), x β€’ c)
def continuous_linear_equiv.pi_ring {π•œ : Type u} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] {X : Type u_1} [topological_space X] [finite_dimensional π•œ E] {f : X β†’ (E β†’L[π•œ] F)} {s : set X} :
continuous_on f s ↔ βˆ€ (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} [nontrivially_normed_field π•œ] {E : Type v} [normed_add_comm_group E] [normed_space π•œ E] {F : Type w} [normed_add_comm_group F] [normed_space π•œ F] [complete_space π•œ] {X : Type u_1} [topological_space X] [finite_dimensional π•œ E] {f : X β†’ (E β†’L[π•œ] F)} :
continuous f ↔ βˆ€ (y : E), continuous (Ξ» (x : X), ⇑(f x) y)
theorem finite_dimensional.proper (π•œ : Type u) [nontrivially_normed_field π•œ] (E : Type v) [normed_add_comm_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.

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.

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} [normed_add_comm_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_add_comm_group E] [complete_space E] [normed_add_comm_group F] [normed_space ℝ F] [finite_dimensional ℝ F] {f : ΞΉ β†’ E} {g : ΞΉ β†’ F} (hg : summable g) (h : f =O[filter.cofinite] g) :