HepLean Documentation

Mathlib.Analysis.Normed.Module.FiniteDimension

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

FiniteDimensional.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_finiteDimensional : a finite-dimensional subspace over a complete field is closed
FiniteDimensional.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 FiniteDimensional.complete on ℝ or ℂ.
FiniteDimensional.of_isCompact_closedBall: 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 LinearMap.continuous_of_finiteDimensional. This gives the desired norm equivalence.

def LinearIsometry.toLinearIsometryEquiv {F : Type u_1} {E₁ : Type u_2} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_3} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.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

li.toLinearIsometryEquiv h = { toLinearEquiv := li.linearEquivOfInjective ⋯ h, norm_map' := ⋯ }

Instances For

@[simp]

theorem LinearIsometry.coe_toLinearIsometryEquiv {F : Type u_1} {E₁ : Type u_2} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_3} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.finrank R₁ F) :

⇑(li.toLinearIsometryEquiv h) = ⇑li

@[simp]

theorem LinearIsometry.toLinearIsometryEquiv_apply {F : Type u_1} {E₁ : Type u_2} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_3} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.finrank R₁ F) (x : E₁) :

(li.toLinearIsometryEquiv h) x = li x

def AffineIsometry.toAffineIsometryEquiv {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedField 𝕜] [NormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [MetricSpace P₁] [PseudoMetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [FiniteDimensional 𝕜 V₁] [FiniteDimensional 𝕜 V₂] [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂) :

P₁ ≃ᵃⁱ[𝕜] P₂

An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.

Equations

li.toAffineIsometryEquiv h = AffineIsometryEquiv.mk' (⇑li) (li.linearIsometry.toLinearIsometryEquiv h) default ⋯

Instances For

@[simp]

theorem AffineIsometry.coe_toAffineIsometryEquiv {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedField 𝕜] [NormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [MetricSpace P₁] [PseudoMetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [FiniteDimensional 𝕜 V₁] [FiniteDimensional 𝕜 V₂] [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂) :

⇑(li.toAffineIsometryEquiv h) = ⇑li

@[simp]

theorem AffineIsometry.toAffineIsometryEquiv_apply {𝕜 : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedField 𝕜] [NormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [MetricSpace P₁] [PseudoMetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] [FiniteDimensional 𝕜 V₁] [FiniteDimensional 𝕜 V₂] [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂) (x : P₁) :

(li.toAffineIsometryEquiv h) x = li x

theorem AffineMap.continuous_of_finiteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE →ᵃ[𝕜] PF) :

Continuous ⇑f

theorem AffineEquiv.continuous_of_finiteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF) :

Continuous ⇑f

def AffineEquiv.toHomeomorphOfFiniteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF) :

PE ≃ₜ PF

Reinterpret an affine equivalence as a homeomorphism.

Equations

f.toHomeomorphOfFiniteDimensional = { toEquiv := f.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[simp]

theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF) :

⇑f.toHomeomorphOfFiniteDimensional = ⇑f

@[simp]

theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF) :

⇑f.toHomeomorphOfFiniteDimensional.symm = ⇑f.symm

theorem ContinuousLinearMap.continuous_det {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] :

Continuous fun (f : E →L[𝕜] E) => f.det

@[irreducible]

def lipschitzExtensionConstant (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] :

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 lipschitzExtensionConstant E'.

Equations

lipschitzExtensionConstant = wrapped✝.1

Instances For

theorem lipschitzExtensionConstant_def (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] :

lipschitzExtensionConstant E' = let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; ‖↑A.symm‖₊ * ‖↑A‖₊ ⊔ 1

theorem lipschitzExtensionConstant_pos (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] :

0 < lipschitzExtensionConstant E'

theorem LipschitzOnWith.extend_finite_dimension {α : Type u_1} [PseudoMetricSpace α] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'} {K : NNReal} (hf : LipschitzOnWith K f s) :

∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s

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 lipschitzExtensionConstant E' * K.

theorem LinearMap.exists_antilipschitzWith {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) (hf : LinearMap.ker f = ⊥) :

∃ K > 0, AntilipschitzWith K ⇑f

theorem LinearMap.injective_iff_antilipschitz {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) :

Function.Injective ⇑f ↔ ∃ K > 0, AntilipschitzWith K ⇑f

A LinearMap on a finite-dimensional space over a complete field is injective iff it is anti-Lipschitz.

theorem ContinuousLinearMap.isOpen_injective {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] :

IsOpen {L : E →L[𝕜] F | Function.Injective ⇑L}

The set of injective continuous linear maps E → F is open, if E is finite-dimensional over a complete field.

theorem LinearIndependent.eventually {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] {f : ι → E} (hf : LinearIndependent 𝕜 f) :

∀ᶠ (g : ι → E) in nhds f, LinearIndependent 𝕜 g

theorem isOpen_setOf_linearIndependent {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] :

IsOpen {f : ι → E | LinearIndependent 𝕜 f}

theorem isOpen_setOf_nat_le_rank {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] (n : ℕ) :

IsOpen {f : E →L[𝕜] F | ↑n ≤ (↑f).rank}

theorem Basis.opNNNorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : NNReal) (hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M) :

‖u‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M

@[deprecated Basis.opNNNorm_le]

theorem Basis.op_nnnorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : NNReal) (hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M) :

‖u‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M

Alias of Basis.opNNNorm_le.

theorem Basis.opNorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ} (hM : 0 ≤ M) (hu : ∀ (i : ι), ‖u (v i)‖ ≤ M) :

‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M

@[deprecated Basis.opNorm_le]

theorem Basis.op_norm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ} (hM : 0 ≤ M) (hu : ∀ (i : ι), ‖u (v i)‖ ≤ M) :

‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M

Alias of Basis.opNorm_le.

theorem Basis.exists_opNNNorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Basis ι 𝕜 E) :

∃ C > 0, ∀ {u : E →L[𝕜] F} (M : NNReal), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

A weaker version of Basis.opNNNorm_le that abstracts away the value of C.

@[deprecated Basis.exists_opNNNorm_le]

theorem Basis.exists_op_nnnorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Basis ι 𝕜 E) :

∃ C > 0, ∀ {u : E →L[𝕜] F} (M : NNReal), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Alias of Basis.exists_opNNNorm_le.

A weaker version of Basis.opNNNorm_le that abstracts away the value of C.

theorem Basis.exists_opNorm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Basis ι 𝕜 E) :

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

A weaker version of Basis.opNorm_le that abstracts away the value of C.

@[deprecated Basis.exists_opNorm_le]

theorem Basis.exists_op_norm_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Basis ι 𝕜 E) :

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

Alias of Basis.exists_opNorm_le.

A weaker version of Basis.opNorm_le that abstracts away the value of C.

instance instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] [SecondCountableTopology F] :

SecondCountableTopology (E →L[𝕜] F)

Equations

⋯ = ⋯

theorem AffineSubspace.closed_of_finiteDimensional {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {P : Type u_1} [MetricSpace P] [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 ↥s.direction] :

theorem exists_norm_le_le_norm_sub_of_finset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) (h : ¬FiniteDimensional 𝕜 E) (s : Finset E) :

∃ (x : E), ‖x‖ ≤ R ∧ ∀ 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} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) (h : ¬FiniteDimensional 𝕜 E) :

∃ (f : ℕ → E), (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (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} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] (h : ¬FiniteDimensional 𝕜 E) :

∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) => 1 ≤ ‖f m - f n‖

theorem FiniteDimensional.of_isCompact_closedBall₀ (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall 0 r)) :

FiniteDimensional 𝕜 E

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.

@[deprecated FiniteDimensional.of_isCompact_closedBall₀]

theorem finiteDimensional_of_isCompact_closedBall₀ (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall 0 r)) :

FiniteDimensional 𝕜 E

Alias of FiniteDimensional.of_isCompact_closedBall₀.

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 FiniteDimensional.of_isCompact_closedBall (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) :

FiniteDimensional 𝕜 E

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

@[deprecated FiniteDimensional.of_isCompact_closedBall]

theorem finiteDimensional_of_isCompact_closedBall (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) :

FiniteDimensional 𝕜 E

Alias of FiniteDimensional.of_isCompact_closedBall.

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

theorem FiniteDimensional.of_locallyCompactSpace (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [LocallyCompactSpace E] :

FiniteDimensional 𝕜 E

Riesz's theorem: a locally compact normed vector space is finite-dimensional.

@[deprecated FiniteDimensional.of_locallyCompactSpace]

theorem finiteDimensional_of_locallyCompactSpace (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [LocallyCompactSpace E] :

FiniteDimensional 𝕜 E

Alias of FiniteDimensional.of_locallyCompactSpace.

Riesz's theorem: a locally compact normed vector space is finite-dimensional.

theorem HasCompactSupport.eq_zero_or_finiteDimensional (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {X : Type u_1} [TopologicalSpace X] [Zero X] [T1Space X] {f : E → X} (hf : HasCompactSupport f) (h'f : Continuous f) :

f = 0 ∨ FiniteDimensional 𝕜 E

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

theorem HasCompactMulSupport.eq_one_or_finiteDimensional (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {X : Type u_1} [TopologicalSpace X] [One X] [T1Space X] {f : E → X} (hf : HasCompactMulSupport f) (h'f : Continuous f) :

f = 1 ∨ FiniteDimensional 𝕜 E

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

theorem ProperSpace.of_locallyCompactSpace (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] :

A locally compact normed vector space is proper.

theorem ProperSpace.of_locallyCompact_module (𝕜 : Type u) [NontriviallyNormedField 𝕜] (E : Type v) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [Nontrivial E] [LocallyCompactSpace E] :

ProperSpace 𝕜

def ContinuousLinearEquiv.piRing {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] (ι : Type u_1) [Fintype ι] [DecidableEq ι] :

((ι → 𝕜) →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

ContinuousLinearEquiv.piRing ι = { toLinearEquiv := LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜), continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

theorem continuousOn_clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {X : Type u_1} [TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} {s : Set X} :

ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun (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} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {X : Type u_1} [TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} :

Continuous f ↔ ∀ (y : E), Continuous fun (x : X) => (f x) y

theorem FiniteDimensional.proper (𝕜 : Type u) [NontriviallyNormedField 𝕜] (E : Type v) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :

Any finite-dimensional vector space over a locally compact 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 900]

instance FiniteDimensional.proper_real (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :

Equations

⋯ = ⋯

instance instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] (S : Submodule 𝕜 E) :

ProperSpace ↥S

A submodule of a locally compact space over a complete field is also locally compact (and even proper).

Equations

⋯ = ⋯

theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ Set.univ) :

∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y

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.infDist x sᶜ from x. See also IsCompact.exists_mem_frontier_infDist_compl_eq_dist.

theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K) (hx : x ∈ K) :

∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y

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.infDist x Kᶜ from x. See also exists_mem_frontier_infDist_compl_eq_dist.

theorem summable_norm_iff {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : α → E} :

(Summable fun (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.norm {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : α → E} :

Summable f → Summable fun (x : α) => ‖f x‖

Alias of the reverse direction of summable_norm_iff.

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_isBigO' {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F} (hg : Summable g) (h : f =O[Filter.cofinite] g) :

theorem Asymptotics.IsBigO.comp_summable {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [CompleteSpace F] {f : E → F} (hf : f =O[nhds 0] id) {g : ι → E} (hg : Summable g) :

Summable (f ∘ g)

theorem summable_of_isBigO_nat' {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F} (hg : Summable g) (h : f =O[Filter.atTop] g) :

theorem summable_of_isEquivalent {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ι → E} (hg : Summable g) (h : Asymptotics.IsEquivalent Filter.cofinite f g) :

theorem summable_of_isEquivalent_nat {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ℕ → E} (hg : Summable g) (h : Asymptotics.IsEquivalent Filter.atTop f g) :

theorem IsEquivalent.summable_iff {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ι → E} (h : Asymptotics.IsEquivalent Filter.cofinite f g) :

Summable f ↔ Summable g

theorem IsEquivalent.summable_iff_nat {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ℕ → E} (h : Asymptotics.IsEquivalent Filter.atTop f g) :

Summable f ↔ Summable g