Documentation

TauCeti.Analysis.InnerProductSpace.Trace.OpNorm

The trace of an operator on a finite-dimensional inner product space #

On a finite-dimensional inner product space V over ℝ or ℂ, the trace of a continuous endomorphism is bounded by the dimension times its operator norm: ‖tr T‖ ≤ dim V * ‖T‖ (ContinuousLinearMap.norm_traceCLM_le). Expanding the trace in an orthonormal basis (bᵢ) gives tr T = ∑ᵢ ⟪bᵢ, T bᵢ⟫, and each term is at most ‖T‖.

This is the bound that controls a non-divergence-form operator tr (A ∘ D²u) by the operator norms of its coefficient field A and of the Hessian D²u.

Restricting to the range gives the sharper estimate ‖tr T‖ ≤ rank T * ‖T‖ (ContinuousLinearMap.norm_traceCLM_le_finrank_range_mul). It applies without self-adjointness or normality and controls traces of low-rank perturbations.

theorem ContinuousLinearMap.norm_traceCLM_le {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →L[𝕜] V) :

The trace of a continuous endomorphism of a finite-dimensional inner product space is bounded by the dimension times the operator norm: ‖tr T‖ ≤ dim V * ‖T‖.

theorem ContinuousLinearMap.norm_traceCLM_le_finrank_range_mul {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →L[𝕜] V) :
‖(TauCeti.traceCLM 𝕜 V) T‖ ≤ ↑(Module.finrank 𝕜 ↥(↑T).range) * ‖T‖

The trace is bounded by the rank times the operator norm, without any normality hypothesis. In particular, low-rank operators have dimension-independent trace bounds.