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' := ⋯ }

@[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 ⋯

@[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 := ⋯ }

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

theorem lipschitzExtensionConstant_def (E' : Type u_1) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] : lipschitzExtensionConstant E' = have A := (Module.Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; max (‖↑A.symm‖₊ * ‖↑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 E' = have A := (Module.Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; max (‖↑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 : 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 isOpen_setOf_affineIndependent {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] : IsOpen {p : ι → E | AffineIndependent 𝕜 p}

theorem Module.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

theorem Module.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

theorem Module.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.

theorem Module.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.

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)

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] : 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.

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.

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.

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.

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 := ⋯ }

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 900]

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

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

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_sum_range_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} {f : ℕ → E} (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) : Summable f

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_norm_mul_geometric_of_norm_lt_one' {F : Type u_1} [NormedRing F] [NormOneClass F] [NormMulClass F] {k : ℕ} {r : F} (hr : ‖r‖ < 1) {u : ℕ → F} (hu : u =O[Filter.atTop] fun (n : ℕ) => ↑(n ^ k)) : Summable fun (n : ℕ) => ‖u n * r ^ n‖

This is a version of summable_norm_mul_geometric_of_norm_lt_one for more general codomains. We keep the original one due to import restrictions.

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

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

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

theorem Module.Basis.continuous_coe_repr {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [NontriviallyNormedField R] [CompleteSpace R] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [Module R M] [ContinuousSMul R M] (B : Basis ι R M) : Continuous fun (m : M) => ⇑(B.repr m)

theorem Module.Basis.continuous_toMatrix {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [NontriviallyNormedField R] [CompleteSpace R] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [Module R M] [ContinuousSMul R M] (B : Basis ι R M) : Continuous fun (v : ι → M) => B.toMatrix v