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

• LinearIsometry.toLinearIsometryEquiv li h = { toLinearEquiv := LinearMap.linearEquivOfInjective li.toLinearMap ⋯ h, norm_map' := ⋯ }

@[simp]

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

@[simp]

theorem LinearIsometry.toLinearIsometryEquiv_apply {F : Type u_2} {E₁ : Type u_3} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F) (x : E₁) : (LinearIsometry.toLinearIsometryEquiv li 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 : FiniteDimensional.finrank 𝕜 V₁ = FiniteDimensional.finrank 𝕜 V₂) : P₁ ≃ᵃⁱ[𝕜] P₂

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

Equations

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

@[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 : FiniteDimensional.finrank 𝕜 V₁ = FiniteDimensional.finrank 𝕜 V₂) : ⇑(AffineIsometry.toAffineIsometryEquiv li 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 : FiniteDimensional.finrank 𝕜 V₁ = FiniteDimensional.finrank 𝕜 V₂) (x : P₁) : (AffineIsometry.toAffineIsometryEquiv li 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

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

@[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) : ⇑(AffineEquiv.toHomeomorphOfFiniteDimensional f) = ⇑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) : ⇑(Homeomorph.symm (AffineEquiv.toHomeomorphOfFiniteDimensional f)) = ⇑(AffineEquiv.symm f)

theorem ContinuousLinearMap.continuous_det {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] : Continuous fun (f : E →L[𝕜] E) => ContinuousLinearMap.det f

theorem lipschitzExtensionConstant_def (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] : lipschitzExtensionConstant E' = let A := LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E')); max (‖↑(ContinuousLinearEquiv.symm A)‖₊ * ‖↑A‖₊) 1

@[irreducible]

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

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

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 ≤ LinearMap.rank ↑f}

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 ι • ‖↑(Basis.equivFunL v)‖₊ * 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 ι • ‖↑(Basis.equivFunL v)‖₊ * 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 ι • ‖↑(Basis.equivFunL v)‖ * 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 ι • ‖↑(Basis.equivFunL v)‖ * 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 instSecondCountableTopologyContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToModuleTopologicalSpaceToAddCommGroupToAddCommGroupToTopologicalAddGroup {𝕜 : 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 𝕜 ↥(AffineSubspace.direction s)] : IsClosed ↑s

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] : ProperSpace E

A locally compact normed vector space is proper.

@[deprecated ProperSpace.of_locallyCompactSpace]

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

Alias of ProperSpace.of_locallyCompactSpace.

---

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 𝕜

@[deprecated ProperSpace.of_locallyCompact_module]

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

Alias of ProperSpace.of_locallyCompact_module.

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

• One or more equations did not get rendered due to their size.

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] : ProperSpace 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 FiniteDimensional.proper_real (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ProperSpace E

Equations

• ⋯ = ⋯

instance instProperSpaceSubtypeMemSubmoduleToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToAddCommMonoidToAddCommGroupToModuleToSeminormedAddCommGroupInstMembershipSetLikePseudoMetricSpaceToPseudoMetricSpace {𝕜 : 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) : Summable f

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

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

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

theorem IsEquivalent.summable_iff {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ι → E} {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 : ℕ → E} {g : ℕ → E} (h : Asymptotics.IsEquivalent Filter.atTop f g) : Summable f ↔ Summable g