Bounded operators on a finite-dimensional space

A bounded operator on a finite-dimensional normed space is just a linear map, so its spectrum is the finite set of eigenvalues. This holds over every field of scalars acting compatibly, for instance over ℝ for an operator on a complex space.

Bounded operators out of a finite-dimensional space are determined by the images of a basis, with operator norm controlled by the norms of those images. Hence such operators into E are approximated in operator norm by operators factoring through any operator g : F →L[𝕜] E of dense range. On a finite-dimensional real domain, strict pointwise norm bounds are equivalent to strict operator-norm bounds.

Bounded operators between finite-dimensional spaces form a finite-dimensional space over every finite extension of the scalars acting compatibly on the codomain, for instance over ℂ for real-linear operators into a complex space.

Main results

• ContinuousLinearMap.finite_spectrum: a bounded operator on a finite-dimensional normed space has finite spectrum, also over subfields of the scalars such as ℝ ⊆ ℂ.
• ContinuousLinearMap.denseRange_comp: on operators out of a finite-dimensional space, postcomposition with an operator of dense range has dense range.
• ContinuousLinearMap.opNorm_lt_iff: a strict norm bound can be checked on every nonzero vector of a finite-dimensional real domain.
• ContinuousLinearMap.finiteDimensional_of_isScalarTower: E →L[𝕜] F is finite-dimensional over a finite extension 𝕜' of 𝕜 acting on a finite-dimensional codomain F.
• IsCompact.isCompact_setOfPred_mapsTo: out of a finite-dimensional space over a complete field, the operators sending a neighbourhood of 0 into a compact set form a compact set.

theorem ContinuousLinearMap.finite_spectrum {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (S : Type u_3) [Field S] [Algebra S 𝕜] [Algebra S (V →L[𝕜] V)] [IsScalarTower S 𝕜 (V →L[𝕜] V)] (T : V →L[𝕜] V) : (spectrum S T).Finite

A bounded operator on a finite-dimensional normed space has finite spectrum over any field S of scalars acting compatibly, for instance over ℝ for an operator on a complex space.

theorem ContinuousLinearMap.denseRange_comp {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : F →L[𝕜] E} (hg : DenseRange ⇑g) : DenseRange g.comp

On continuous linear maps out of a finite-dimensional space, postcomposition with a continuous linear map of dense range has dense range: each T : V →L[𝕜] E is approximated in operator norm by maps g.comp U with U : V →L[𝕜] F.

theorem ContinuousLinearMap.opNorm_lt_iff {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [SeminormedAddCommGroup F] [NormedSpace ℝ F] (A : E →L[ℝ] F) {c : ℝ} (hc : 0 < c) : ‖A‖ < c ↔ ∀ (x : E), x ≠ 0 → ‖A x‖ < c * ‖x‖

On a finite-dimensional real domain, a strict pointwise operator bound gives a strict operator-norm bound. The positivity assumption includes the zero-dimensional domain.

theorem ContinuousLinearMap.finiteDimensional_of_isScalarTower {𝕜 : Type u_3} {𝕜' : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [FiniteDimensional 𝕜 𝕜'] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜' F] [NormedSpace 𝕜 F] [IsScalarTower 𝕜 𝕜' F] [FiniteDimensional 𝕜' F] : FiniteDimensional 𝕜' (E →L[𝕜] F)

Bounded 𝕜-linear operators between finite-dimensional spaces form a finite-dimensional space over a finite extension 𝕜' of 𝕜 acting compatibly on the codomain, for instance over ℂ for real-linear operators into a finite-dimensional complex space.

theorem IsCompact.isCompact_setOfPred_mapsTo {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {K : Set F} (hK : IsCompact K) {s : Set E} (hs : s ∈ nhds 0) : IsCompact {T : E →L[𝕜] F | Set.MapsTo (⇑T) s K}

Out of a finite-dimensional normed space over a complete field, the operators sending a neighbourhood s of 0 into a compact set K form a compact set.