Exact source: Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Finite-dimensionality transfers across a sphere isometry
1/-2Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Sébastien Gouëzel5-/6module78public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent9public import Mathlib.Analysis.Normed.Group.Lemmas10public import Mathlib.Analysis.Normed.Affine.Isometry11public import Mathlib.Analysis.Normed.Operator.NormedSpace12public import Mathlib.Analysis.Normed.Module.RieszLemma13public import Mathlib.Analysis.Normed.Module.Ball.Pointwise14public import Mathlib.Analysis.SpecificLimits.Normed15public import Mathlib.Logic.Encodable.Pi16public import Mathlib.Topology.Algebra.AffineSubspace17public import Mathlib.Topology.Algebra.Module.FiniteDimension18public import Mathlib.Topology.Algebra.InfiniteSum.Module19public import Mathlib.Topology.Instances.Matrix20public import Mathlib.LinearAlgebra.Dimension.LinearMap21public import Mathlib.LinearAlgebra.Dual.Lemmas222324/-!25# Finite-dimensional normed spaces over complete fields2627Over a complete nontrivially normed field, in finite dimension, all norms are equivalent and all28linear maps are continuous. Moreover, a finite-dimensional subspace is always complete and closed.2930## Main results:3132* `FiniteDimensional.complete` : a finite-dimensional space over a complete field is complete. This33 is not registered as an instance, as the field would be an unknown metavariable in typeclass34 resolution.35* `Submodule.closed_of_finiteDimensional` : a finite-dimensional subspace over a complete field is36 closed37* `FiniteDimensional.proper` : a finite-dimensional space over a proper field is proper. This38 is not registered as an instance, as the field would be an unknown metavariable in typeclass39 resolution. It is however registered as an instance for `𝕜 = ℝ` and `𝕜 = ℂ`. As properness40 implies completeness, there is no need to also register `FiniteDimensional.complete` on `ℝ` or41 `ℂ`.42* `FiniteDimensional.of_isCompact_closedBall`: Riesz' theorem: if the closed unit ball is43 compact, then the space is finite-dimensional.4445## Implementation notes4647The fact that all norms are equivalent is not written explicitly, as it would mean having two norms48on a single space, which is not the way type classes work. However, if one has a49finite-dimensional vector space `E` with a norm, and a copy `E'` of this type with another norm,50then the identities from `E` to `E'` and from `E'` to `E` are continuous thanks to51`LinearMap.continuous_of_finiteDimensional`. This gives the desired norm equivalence.52-/5354@[expose] public section5556universe u v w x5758noncomputable section5960open Asymptotics Filter Module Metric Module NNReal Set TopologicalSpace Topology6162namespace LinearIsometry6364open LinearMap6566variable {F E₁ : Type*} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁]67variable {R₁ : Type*} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁]68 [FiniteDimensional R₁ F]6970/-- A linear isometry between finite-dimensional spaces of equal dimension can be upgraded71to a linear isometry equivalence. -/72def toLinearIsometryEquiv (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) :73 E₁ ≃ₗᵢ[R₁] F where74 toLinearEquiv := li.toLinearMap.linearEquivOfInjective li.injective h75 norm_map' := li.norm_map'7677@[simp]78theorem coe_toLinearIsometryEquiv (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) :79 (li.toLinearIsometryEquiv h : E₁ → F) = li :=80 rfl8182@[simp]83theorem toLinearIsometryEquiv_apply (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F)84 (x : E₁) : (li.toLinearIsometryEquiv h) x = li x :=85 rfl8687end LinearIsometry8889namespace AffineIsometry9091open AffineMap9293variable {𝕜 : Type*} {V₁ V₂ : Type*} {P₁ P₂ : Type*} [NormedField 𝕜] [NormedAddCommGroup V₁]94 [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₁] [NormedSpace 𝕜 V₂] [MetricSpace P₁]95 [PseudoMetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂]9697variable [FiniteDimensional 𝕜 V₁] [FiniteDimensional 𝕜 V₂]9899/-- An affine isometry between finite-dimensional spaces of equal dimension can be upgraded100to an affine isometry equivalence. -/101def toAffineIsometryEquiv [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) :102 P₁ ≃ᵃⁱ[𝕜] P₂ :=103 AffineIsometryEquiv.mk' li (li.linearIsometry.toLinearIsometryEquiv h)104 (Inhabited.default (α := P₁)) fun p => by simp105106@[simp]107theorem coe_toAffineIsometryEquiv [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂)108 (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) : (li.toAffineIsometryEquiv h : P₁ → P₂) = li :=109 rfl110111@[simp]112theorem toAffineIsometryEquiv_apply [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂)113 (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) (x : P₁) : (li.toAffineIsometryEquiv h) x = li x :=114 rfl115116end AffineIsometry117118section CompleteField119120variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E]121 [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜]122123section Affine124125variable {PE PF : Type*} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF]126 [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E]127128theorem AffineMap.continuous_of_finiteDimensional (f : PE →ᵃ[𝕜] PF) : Continuous f :=129 AffineMap.continuous_linear_iff.1 f.linear.continuous_of_finiteDimensional130131theorem AffineEquiv.continuous_of_finiteDimensional (f : PE ≃ᵃ[𝕜] PF) : Continuous f :=132 f.toAffineMap.continuous_of_finiteDimensional133134/-- Reinterpret an affine equivalence as a continuous affine equivalence in finite dimension. -/135def AffineEquiv.toContinuousAffineEquiv : (PE ≃ᵃ[𝕜] PF) ≃ (PE ≃ᴬ[𝕜] PF) where136 toFun f :=137 haveI := f.linear.finiteDimensional138 ⟨f, f.continuous_of_finiteDimensional, f.symm.continuous_of_finiteDimensional⟩139 invFun f := f.toAffineEquiv140 left_inv _ := rfl141 right_inv _ := ContinuousAffineEquiv.toAffineEquiv_injective rfl142143@[simp]144theorem AffineEquiv.coe_toContinuousAffineEquiv (f : PE ≃ᵃ[𝕜] PF) :145 ⇑(toContinuousAffineEquiv f) = f := rfl146147@[simp]148theorem AffineEquiv.toAffineEquiv_toContinuousAffineEquiv (f : PE ≃ᵃ[𝕜] PF) :149 (toContinuousAffineEquiv f).toAffineEquiv = f := rfl150151@[simp]152theorem AffineEquiv.toContinuousAffineEquiv_symm_apply (f : PE ≃ᴬ[𝕜] PF) :153 toContinuousAffineEquiv.symm f = f.toAffineEquiv := rfl154155/-- Reinterpret an affine equivalence as a homeomorphism. -/156def AffineEquiv.toHomeomorphOfFiniteDimensional (f : PE ≃ᵃ[𝕜] PF) : PE ≃ₜ PF :=157 (toContinuousAffineEquiv f).toHomeomorph158159@[simp]160theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional (f : PE ≃ᵃ[𝕜] PF) :161 ⇑f.toHomeomorphOfFiniteDimensional = f :=162 rfl163164@[simp]165theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm (f : PE ≃ᵃ[𝕜] PF) :166 ⇑f.toHomeomorphOfFiniteDimensional.symm = f.symm :=167 rfl168169attribute [deprecated AffineEquiv.toContinuousAffineEquiv (since := "2026-05-11")]170 AffineEquiv.toHomeomorphOfFiniteDimensional171172/-- An affine map from a finite-dimensional space is automatically Lipschitz. -/173theorem AffineMap.lipschitzWith_of_finiteDimensional (f : PE →ᵃ[𝕜] PF) :174 ∃ K : ℝ≥0, LipschitzWith K f := by175 let fL : E →L[𝕜] F := f.linear.toContinuousLinearMap176 refine ⟨‖fL‖₊, LipschitzWith.of_dist_le_mul fun x y ↦ ?_⟩177 rw [NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm', ← f.linearMap_vsub]178 exact fL.le_opNorm _179180end Affine181182theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E => f.det := by183 change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)184 -- TODO: this could be easier with `det_cases`185 by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)186 · rcases h with ⟨s, ⟨b⟩⟩187 haveI : FiniteDimensional 𝕜 E := b.finiteDimensional_of_finite188 classical189 simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]190 refine Continuous.matrix_det ?_191 exact192 ((LinearMap.toMatrix b b).toLinearMap.comp193 (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional194 · rw [LinearMap.det]195 simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const196197/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real198vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse199constant `C * K` where `C` only depends on `E'`. We record a working value for this constant `C`200as `lipschitzExtensionConstant E'`. -/201irreducible_def lipschitzExtensionConstant (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']202 [FiniteDimensional ℝ E'] : ℝ≥0 :=203 let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv204 max (‖A.symm.toContinuousLinearMap‖₊ * ‖A.toContinuousLinearMap‖₊) 1205206theorem lipschitzExtensionConstant_pos (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']207 [FiniteDimensional ℝ E'] : 0 < lipschitzExtensionConstant E' := by208 rw [lipschitzExtensionConstant]209 exact zero_lt_one.trans_le (le_max_right _ _)210211/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real212vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse213constant `lipschitzExtensionConstant E' * K`. -/214theorem LipschitzOnWith.extend_finite_dimension {α : Type*} [PseudoMetricSpace α] {E' : Type*}215 [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'}216 {K : ℝ≥0} (hf : LipschitzOnWith K f s) :217 ∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s := by218 /- This result is already known for spaces `ι → ℝ`. We use a continuous linear equiv between219 `E'` and such a space to transfer the result to `E'`. -/220 let ι : Type _ := Basis.ofVectorSpaceIndex ℝ E'221 let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv222 have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz223 have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=224 LA.comp_lipschitzOnWith hf225 obtain ⟨g, hg, gs⟩ :226 ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=227 L.extend_pi228 refine ⟨A.symm ∘ g, ?_, ?_⟩229 · have LAsymm : LipschitzWith ‖A.symm.toContinuousLinearMap‖₊ A.symm := by230 apply A.symm.lipschitz231 apply (LAsymm.comp hg).weaken232 rw [lipschitzExtensionConstant, ← mul_assoc]233 exact mul_le_mul' (le_max_left _ _) le_rfl234 · intro x hx235 have : A (f x) = g x := gs hx236 simp only [(· ∘ ·), ← this, A.symm_apply_apply]237238theorem LinearMap.exists_antilipschitzWith [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F)239 (hf : LinearMap.ker f = ⊥) : ∃ K > 0, AntilipschitzWith K f := by240 cases subsingleton_or_nontrivial E241 · exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩242 · rw [LinearMap.ker_eq_bot] at hf243 let e : E ≃L[𝕜] LinearMap.range f := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv244 exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩245246open Function in247/-- A `LinearMap` on a finite-dimensional space over a complete field248 is injective iff it is anti-Lipschitz. -/249theorem LinearMap.injective_iff_antilipschitz [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) :250 Injective f ↔ ∃ K > 0, AntilipschitzWith K f := by251 constructor252 · rw [← LinearMap.ker_eq_bot]253 exact f.exists_antilipschitzWith254 · rintro ⟨K, -, H⟩255 exact H.injective256257/-- An injective affine map from a finite-dimensional space is automatically anti-Lipschitz. -/258theorem AffineMap.antilipschitzWith_of_finiteDimensional {PE PF : Type*} [MetricSpace PE]259 [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional 𝕜 E]260 {f : PE →ᵃ[𝕜] PF} (hf : Function.Injective f) :261 ∃ K : ℝ≥0, AntilipschitzWith K f := by262 obtain ⟨K, -, hK⟩ := f.linear.injective_iff_antilipschitz.mp (f.linear_injective_iff.mpr hf)263 refine ⟨K, AntilipschitzWith.of_le_mul_dist fun x y ↦ ?_⟩264 rw [dist_eq_norm_vsub E, dist_eq_norm_vsub F, ← f.linearMap_vsub]265 exact ZeroHomClass.bound_of_antilipschitz f.linear hK (x -ᵥ y)266267open Function in268/-- The set of injective continuous linear maps `E → F` is open,269 if `E` is finite-dimensional over a complete field. -/270theorem ContinuousLinearMap.isOpen_injective [FiniteDimensional 𝕜 E] :271 IsOpen { L : E →L[𝕜] F | Injective L } := by272 rw [isOpen_iff_eventually]273 rintro φ₀ hφ₀274 rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩275 have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_pos276 filter_upwards [this] with φ hφ277 apply φ.injective_iff_antilipschitz.mpr278 exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),279 H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩280281open ContinuousLinearMap282283/-- Continuous linear equivalence between continuous linear functions `𝕜ⁿ → E` and `Eⁿ`.284The spaces `𝕜ⁿ` and `Eⁿ` are represented as `ι → 𝕜` and `ι → E`, respectively,285where `ι` is a finite type. -/286def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :287 ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=288 { LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜) with289 continuous_invFun := by290 simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]291 refine AddMonoidHomClass.continuous_of_bound292 (LinearMap.toContinuousLinearMap.toLinearMap.comp293 (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)294 (Fintype.card ι : ℝ) fun g ↦ ?_295 rw [← nsmul_eq_mul]296 refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t ↦ ?_297 simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,298 LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]299 apply le_trans (norm_sum_le _ _)300 rw [smul_mul_assoc]301 refine Finset.sum_le_card_nsmul _ _ _ fun i _ ↦ ?_302 rw [norm_smul, mul_comm]303 gcongr <;> apply norm_le_pi_norm }304305protected theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}306 (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g := by307 cases nonempty_fintype ι308 classical309 simp only [Fintype.linearIndependent_iff'] at hf ⊢310 rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩311 have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=312 tendsto_finsetSum _ fun i _ =>313 Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds314 simp only [sub_self, norm_zero, Finset.sum_const_zero] at this315 refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_316 replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by317 rw [← NNReal.coe_lt_coe]318 push_cast319 exact hg320 rw [LinearMap.ker_eq_bot]321 refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective322 simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,323 LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←324 Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]325 refine norm_sum_le_of_le _ fun i _ => ?_326 rw [norm_smul, mul_comm]327 gcongr328 exact norm_le_pi_norm (v - u) i329330theorem isOpen_setOf_linearIndependent {ι : Type*} [Finite ι] :331 IsOpen { f : ι → E | LinearIndependent 𝕜 f } :=332 isOpen_iff_mem_nhds.2 fun _ => LinearIndependent.eventually333334theorem isOpen_setOf_nat_le_rank (n : ℕ) :335 IsOpen { f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank } := by336 simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]337 refine isOpen_biUnion fun t _ => ?_338 have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=339 continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous340 exact isOpen_setOf_linearIndependent.preimage this341342theorem isOpen_setOf_affineIndependent {ι : Type*} [Finite ι] :343 IsOpen {p : ι → E | AffineIndependent 𝕜 p} := by344 classical345 rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩346 · exact isOpen_discrete _347 · simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]348 let ι' := { x // x ≠ i₀ }349 cases nonempty_fintype ι350 haveI : Fintype ι' := Subtype.fintype _351 convert_to!352 IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})353 exact isOpen_setOf_linearIndependent.preimage (by fun_prop)354355namespace Module.Basis356357theorem opNNNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : ℝ≥0)358 (hu : ∀ i, ‖u (v i)‖₊ ≤ M) : ‖u‖₊ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊ * M :=359 u.opNNNorm_le_bound _ fun e => by360 set φ := v.equivFunL.toContinuousLinearMap361 calc362 ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]363 _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]364 _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _365 _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]366 _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu367 _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]368 _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by369 gcongr370 calc371 ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _372 _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _373 _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]374375theorem opNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ}376 (hM : 0 ≤ M) (hu : ∀ i, ‖u (v i)‖ ≤ M) :377 ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M := by378 simpa using! NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)379380/-- A weaker version of `Basis.opNNNorm_le` that abstracts away the value of `C`. -/381theorem exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :382 ∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M := by383 cases nonempty_fintype ι384 exact385 ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,386 zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>387 (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) zero_le⟩388389/-- A weaker version of `Basis.opNorm_le` that abstracts away the value of `C`. -/390theorem exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :391 ∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M := by392 obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)393 refine ⟨C, hC, ?_⟩394 intro u M hM H395 simpa using! h ⟨M, hM⟩ H396397end Module.Basis398399instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] :400 SecondCountableTopology (E →L[𝕜] F) := by401 let d := Module.finrank 𝕜 E402 let e₁ : E ≃L[𝕜] Fin d → 𝕜 :=403 ContinuousLinearEquiv.ofFinrankEq (finrank_fin_fun 𝕜).symm404 let e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=405 (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))406 exact e₂.toHomeomorph.secondCountableTopology407408theorem AffineSubspace.closed_of_finiteDimensional {P : Type*} [MetricSpace P]409 [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 s.direction] :410 IsClosed (s : Set P) :=411 s.isClosed_direction_iff.mp s.direction.closed_of_finiteDimensional412413section Riesz414415/-- In an infinite-dimensional space, given a finite number of points, one may find a point416with norm at most `R` which is at distance at least `1` of all these points. -/417theorem exists_norm_le_le_norm_sub_of_finset {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R)418 (h : ¬FiniteDimensional 𝕜 E) (s : Finset E) : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖ := by419 let F := Submodule.span 𝕜 (s : Set E)420 have hF : F.FG := ⟨s, rfl⟩421 haveI : FiniteDimensional 𝕜 F := .of_fg hF422 have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _423 have : ∃ x, x ∉ F := by424 contrapose! h425 have : (⊤ : Submodule 𝕜 E) = F := by426 ext x427 simp [h]428 rw [← this] at hF429 exact .of_fg_top hF430 obtain ⟨x, xR, hx⟩ : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y : E, y ∈ F → 1 ≤ ‖x - y‖ :=431 riesz_lemma_of_norm_lt hc hR Fclosed this432 have hx' : ∀ y : E, y ∈ F → 1 ≤ ‖y - x‖ := by433 intro y hy434 rw [← norm_neg]435 simpa using hx y hy436 exact ⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩437438/-- In an infinite-dimensional normed space, there exists a sequence of points which are all439bounded by `R` and at distance at least `1`. For a version not assuming `c` and `R`, see440`exists_seq_norm_le_one_le_norm_sub`. -/441theorem exists_seq_norm_le_one_le_norm_sub' {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R)442 (h : ¬FiniteDimensional 𝕜 E) :443 ∃ f : ℕ → E, (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ := by444 have : Std.Symm fun x y : E => 1 ≤ ‖x - y‖ := by445 constructor446 intro x y hxy447 rw [← norm_neg]448 simpa449 apply450 exists_seq_of_forall_finset_exists' (fun x : E => ‖x‖ ≤ R) fun (x : E) (y : E) => 1 ≤ ‖x - y‖451 rintro s -452 exact exists_norm_le_le_norm_sub_of_finset hc hR h s453454theorem exists_seq_norm_le_one_le_norm_sub (h : ¬FiniteDimensional 𝕜 E) :455 ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ := by456 obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜457 have A : ‖c‖ < ‖c‖ + 1 := by linarith458 rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩459 exact ⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩460461variable (𝕜)462463/-- **Riesz's theorem**: if a closed ball with center zero of positive radius is compact in a vector464space, then the space is finite-dimensional. -/465theorem FiniteDimensional.of_isCompact_closedBall₀ {V : Type*} [NormedAddCommGroup V] [Module 𝕜 V]466 [ContinuousSMul 𝕜 V] {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall (0 : V) r)) :467 FiniteDimensional 𝕜 V :=468 .of_totallyBounded_nhds_zero 𝕜 (Metric.closedBall_mem_nhds 0 rpos) h.totallyBounded469470/-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the471space is finite-dimensional. -/472theorem FiniteDimensional.of_isCompact_closedBall {V : Type*} [NormedAddCommGroup V] [Module 𝕜 V]473 [ContinuousSMul 𝕜 V] {r : ℝ} (rpos : 0 < r) {c : V} (h : IsCompact (Metric.closedBall c r)) :474 FiniteDimensional 𝕜 V :=475 .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)476477/-- A locally compact normed vector space is proper. -/478lemma ProperSpace.of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*}479 [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] : ProperSpace E := by480 rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩481 rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩482 have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖ ^ n * r)) := fun n ↦ by483 have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc484 simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)485 have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=486 Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)487 exact .of_seq_closedBall hTop (Eventually.of_forall hC)488489lemma ProperSpace.of_locallyCompact_module (V : Type*) [AddCommGroup V] [TopologicalSpace V]490 [IsTopologicalAddGroup V] [T2Space V] [Nontrivial V] [LocallyCompactSpace V] [Module 𝕜 V]491 [ContinuousSMul 𝕜 V] : ProperSpace 𝕜 :=492 have : LocallyCompactSpace 𝕜 := by493 obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 := exists_ne 0494 let L : 𝕜 → V := fun t ↦ t • v495 have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv496 apply IsClosedEmbedding.locallyCompactSpace this497 .of_locallyCompactSpace 𝕜498499end Riesz500501open ContinuousLinearMap502503/-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications504are. -/505theorem continuousWithinAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]506 {f : X → E →L[𝕜] F} {s : Set X} {x : X} :507 ContinuousWithinAt f s x ↔ ∀ y, ContinuousWithinAt (fun q ↦ f q y) s x := by508 refine ⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun h ↦ ?_⟩509 let e : (E →L[𝕜] F) ≃L[𝕜] Fin (finrank 𝕜 E) → F :=510 ((ContinuousLinearEquiv.ofFinrankEq (finrank_fin_fun 𝕜).symm).arrowCongr511 (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing _)512 rw [e.toHomeomorph.isInducing.continuousWithinAt_iff]513 exact continuousWithinAt_pi.mpr fun i ↦ h _514515/-- A family of continuous linear maps is continuous on `s` iff all its applications are. -/516theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]517 {f : X → E →L[𝕜] F} {s : Set X} :518 ContinuousOn f s ↔ ∀ y, ContinuousOn (fun x ↦ f x y) s := by519 simp_rw [ContinuousOn, continuousWithinAt_clm_apply, imp_forall_iff]520 exact forall_comm521522/-- A family of continuous linear maps is continuous at a point iff all its applications are. -/523theorem continuousAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]524 {f : X → E →L[𝕜] F} {x : X} :525 ContinuousAt f x ↔ ∀ y, ContinuousAt (fun q ↦ f q y) x := by526 simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_apply]527528theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]529 {f : X → E →L[𝕜] F} : Continuous f ↔ ∀ y, Continuous (f · y) := by530 simp_rw [← continuousOn_univ, continuousOn_clm_apply]531532end CompleteField533534section LocallyCompactField535536variable (𝕜 : Type u) [NontriviallyNormedField 𝕜] (E : Type v) [NormedAddCommGroup E]537 [NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜]538539/-- Any finite-dimensional vector space over a locally compact field is proper.540We do not register this as an instance to avoid an instance loop when trying to prove the541properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance542explicitly when needed. -/543theorem FiniteDimensional.proper [FiniteDimensional 𝕜 E] : ProperSpace E := by544 have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜545 set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm546 exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective547548end LocallyCompactField549550/-- Over the real numbers, we can register the previous statement as an instance as it will not551cause problems in instance resolution since the properness of `ℝ` is already known. -/552instance (priority := 900) FiniteDimensional.proper_real (E : Type u) [NormedAddCommGroup E]553 [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ProperSpace E :=554 FiniteDimensional.proper ℝ E555556/-- A submodule of a locally compact space over a complete field is also locally compact (and even557proper). -/558instance {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]559 [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] (S : Submodule 𝕜 E) :560 ProperSpace S := by561 nontriviality E562 have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E563 have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜564 exact FiniteDimensional.proper 𝕜 S565566/-- If `E` is a finite-dimensional normed real vector space, `x : E`, and `s` is a neighborhood of567`x` that is not equal to the whole space, then there exists a point `y ∈ frontier s` at distance568`Metric.infDist x sᶜ` from `x`. See also569`IsCompact.exists_mem_frontier_infDist_compl_eq_dist`. -/570theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type*} [NormedAddCommGroup E]571 [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ univ) :572 ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y := by573 rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩574 rw [closure_compl] at hys575 refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|576 Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩577 rwa [dist_comm]578579/-- If `K` is a compact set in a nontrivial real normed space and `x ∈ K`, then there exists a point580`y` of the boundary of `K` at distance `Metric.infDist x Kᶜ` from `x`. See also581`exists_mem_frontier_infDist_compl_eq_dist`. -/582nonrec theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type*}583 [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K)584 (hx : x ∈ K) :585 ∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y := by586 obtain hx' | hx' : x ∈ interior K ∪ frontier K := by587 rw [← closure_eq_interior_union_frontier]588 exact subset_closure hx589 · rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'590 rcases hx' with ⟨r, hr₀, hrK⟩591 have : FiniteDimensional ℝ E :=592 .of_isCompact_closedBall ℝ hr₀593 (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)594 exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ595 · refine ⟨x, hx', ?_⟩596 rw [frontier_eq_closure_inter_closure] at hx'597 rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]598599/-- In a finite-dimensional vector space over `ℝ`, the series `∑ x, ‖f x‖` is unconditionally600summable if and only if the series `∑ x, f x` is unconditionally summable. One implication holds in601any complete normed space, while the other holds only in finite-dimensional spaces. -/602theorem summable_norm_iff {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]603 [FiniteDimensional ℝ E] {f : α → E} : (Summable fun x => ‖f x‖) ↔ Summable f := by604 refine ⟨Summable.of_norm, fun hf ↦ ?_⟩605 -- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ`606 suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by607 obtain v := Module.finBasis ℝ E608 set e := v.equivFunL609 have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)610 refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_611 simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)612 clear! E613 -- Now we deal with `g : α → Fin N → ℝ`614 intro N g hg615 have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs616 refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_617 rw [norm_norm, pi_norm_le_iff_of_nonneg]618 · refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)619 exact norm_nonneg (g x i)620 · exact Finset.sum_nonneg fun _ _ => norm_nonneg _621622alias ⟨_, Summable.norm⟩ := summable_norm_iff623624theorem summable_of_sum_range_norm_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]625 [FiniteDimensional ℝ E] {c : ℝ} {f : ℕ → E} (h : ∀ n, ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) :626 Summable f :=627 summable_norm_iff.mp <| summable_of_sum_range_le (fun _ ↦ norm_nonneg _) h628629theorem summable_of_isBigO' {ι E F : Type*} [NormedAddCommGroup E] [CompleteSpace E]630 [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F}631 (hg : Summable g) (h : f =O[cofinite] g) : Summable f :=632 summable_of_isBigO hg.norm h.norm_right633634lemma Asymptotics.IsBigO.comp_summable {ι E F : Type*}635 [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]636 [NormedAddCommGroup F] [CompleteSpace F]637 {f : E → F} (hf : f =O[𝓝 0] id) {g : ι → E} (hg : Summable g) : Summable (f ∘ g) :=638 .of_norm <| hf.comp_summable_norm hg.norm639640theorem summable_of_isBigO_nat' {E F : Type*} [NormedAddCommGroup E] [CompleteSpace E]641 [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F}642 (hg : Summable g) (h : f =O[atTop] g) : Summable f :=643 summable_of_isBigO_nat hg.norm h.norm_right644645646open Nat Asymptotics in647/-- This is a version of `summable_norm_mul_geometric_of_norm_lt_one` for more general codomains. We648keep the original one due to import restrictions. -/649theorem summable_norm_mul_geometric_of_norm_lt_one' {F : Type*} [NormedRing F]650 [NormOneClass F] [NormMulClass F] {k : ℕ} {r : F} (hr : ‖r‖ < 1) {u : ℕ → F}651 (hu : u =O[atTop] fun n ↦ ((n ^ k : ℕ) : F)) : Summable fun n : ℕ ↦ ‖u n * r ^ n‖ := by652 rcases exists_between hr with ⟨r', hrr', h⟩653 apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h).norm654 calc655 fun n ↦ ‖(u n) * r ^ n‖656 _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by657 apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO658 filter_upwards [eventually_norm_pow_le r] with n hn659 simp660 _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by661 simpa [Nat.cast_pow] using662 (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)663 _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by664 convert!665 isBigO_norm_right.mpr666 (isBigO_norm_left.mpr667 (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)668 simp only [norm_pow, norm_mul]669670theorem summable_of_isEquivalent {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]671 [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E} (hg : Summable g) (h : f ~[cofinite] g) :672 Summable f :=673 summable_of_isBigO' hg h.isBigO674675theorem summable_of_isEquivalent_nat {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]676 [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (hg : Summable g) (h : f ~[atTop] g) :677 Summable f :=678 summable_of_isBigO_nat' hg h.isBigO679680theorem Asymptotics.IsTheta.summable_iff {ι E F : Type*} [NormedAddCommGroup E]681 [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [FiniteDimensional ℝ E]682 [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F} (h : f =Θ[cofinite] g) :683 Summable f ↔ Summable g :=684 ⟨fun hf => summable_of_isBigO' hf h.isBigO_symm, fun hg => summable_of_isBigO' hg h.isBigO⟩685686theorem Asymptotics.IsTheta.summable_iff_nat {E F : Type*} [NormedAddCommGroup E]687 [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [FiniteDimensional ℝ E]688 [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F} (h : f =Θ[atTop] g) :689 Summable f ↔ Summable g :=690 IsTheta.summable_iff <| by simpa [← Nat.cofinite_eq_atTop] using h691692theorem Asymptotics.IsEquivalent.summable_iff {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]693 [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E} (h : f ~[cofinite] g) :694 Summable f ↔ Summable g :=695 h.isTheta.summable_iff696697@[deprecated (since := "2026-02-07")]698alias IsEquivalent.summable_iff := Asymptotics.IsEquivalent.summable_iff699700theorem Asymptotics.IsEquivalent.summable_iff_nat {E : Type*} [NormedAddCommGroup E]701 [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (h : f ~[atTop] g) :702 Summable f ↔ Summable g :=703 h.isTheta.summable_iff_nat704705@[deprecated (since := "2026-02-07")]706alias IsEquivalent.summable_iff_nat := Asymptotics.IsEquivalent.summable_iff_nat707708namespace Module.Basis709710variable {ι R M : Type*} [Finite ι]711 [NontriviallyNormedField R] [CompleteSpace R]712 [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M]713 [Module R M] [ContinuousSMul R M] (B : Module.Basis ι R M)714715-- Note that Finsupp has no topology so we need the coercion, see716-- https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/TVS.20and.20NormedSpace.20on.20Finsupp.2C.20DFinsupp.2C.20DirectSum.2C.20.2E.2E/near/512890984717theorem continuous_coe_repr : Continuous (fun m : M => ⇑(B.repr m)) :=718 have := Finite.of_basis B719 LinearMap.continuous_of_finiteDimensional B.equivFun.toLinearMap720721-- Note: this could be generalized if we had some typeclass to indicate "each of the projections722-- into the basis is continuous".723theorem continuous_toMatrix : Continuous fun (v : ι → M) => B.toMatrix v :=724 let _ := Fintype.ofFinite ι725 have := Finite.of_basis B726 LinearMap.continuous_of_finiteDimensional B.toMatrixEquiv.toLinearMap727728end Module.Basis