Pointwise convergence of endomorphisms in finite dimension

Let $E$ be a finite-dimensional complex normed space and let $S_N$ and $P$ be continuous linear endomorphisms of $E$. If $S_N(x)\to P(x)$ for every $x\in E$, then $S_N\to P$ in the operator norm.

Evaluation on a finite basis identifies the endomorphisms of $E$ with a finite product of copies of $E$, linearly and bijectively. In finite dimension both directions of this identification are continuous, so coordinatewise convergence of the evaluations transports back to convergence of the maps themselves.

Main statements

• ContinuousLinearMap.tendsto_of_tendsto_apply_of_finiteDimensional: pointwise convergence of continuous linear endomorphisms of a finite-dimensional space implies convergence in the operator norm.
• ContinuousLinearMap.tendsto_trace_pow_of_tendsto_zero: the traces of powers converge to zero whenever the powers converge to zero in operator norm.

theorem ContinuousLinearMap.tendsto_of_tendsto_apply_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {S : ℕ → E →L[ℂ] E} {P : E →L[ℂ] E} (h : ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => (S n) x) Filter.atTop (nhds (P x))) : Filter.Tendsto S Filter.atTop (nhds P)

In finite dimension, pointwise convergence of continuous linear endomorphisms implies convergence in the operator norm: evaluation on a finite basis is a linear isomorphism onto a finite product, hence a homeomorphism.

theorem ContinuousLinearMap.tendsto_trace_pow_of_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (F : E →L[ℂ] E) (hF : Filter.Tendsto (fun (n : ℕ) => F ^ n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (LinearMap.trace ℂ E) ↑(F ^ n)) Filter.atTop (nhds 0)

If the powers of an endomorphism converge to zero in operator norm, then their linear-map traces converge to zero.