mathlib3 documentation

analysis.normed_space.finite_dimension

Finite dimensional normed spaces over complete fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Reinterpret an affine equivalence as a homeomorphism.

Equations
@[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.

@[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 f.rank}
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.

A finite-dimensional subspace is complete.

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) :
(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} [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) :
(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} [nontrivially_normed_field 𝕜] {E : Type v} [normed_add_comm_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

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.

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

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

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

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)

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 exists_mem_frontier_inf_dist_compl_eq_dist {E : Type u_1} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {x : E} {s : set E} (hx : x s) (hs : s set.univ) :

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.

theorem is_compact.exists_mem_frontier_inf_dist_compl_eq_dist {E : Type u_1} [normed_add_comm_group E] [normed_space E] [nontrivial E] {x : E} {K : set E} (hK : is_compact K) (hx : x K) :

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