Excess-support compression provider bridges

This module proves the reusable algebraic bridge behind the ambient identity excess-support fallback: if matrixExp A is support-dominated by support and the support itself is bounded above by the identity, then the excess part matrixExp A - 1 is dominated by (exp (lambdaMaxOrdered A hA) - 1) 闂?support.

It does not construct smaller support projections, prove effective-rank bounds, or prove any Lieb or Matrix Bernstein fact.

theorem HighDimProb.matrixExpExcessSupportDomination_of_supportDomination_of_support_le_one {n : ℕ} {A support : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hA : IsSelfAdjointMatrix A) (hDom : MatrixExpSupportDomination A support hA) (hSupportLeOne : support ≤ 1) : MatrixExpExcessSupportDomination A support hA

Compress a support-domination certificate into an excess-support certificate whenever the support is bounded above by the ambient identity.

This is the reusable algebraic bridge behind the identity excess-support fallback: the hard spectral work remains in MatrixExpSupportDomination, while support <= 1 lets us replace -1 by -support on the right-hand side and rewrite the result as (exp (lambdaMaxOrdered A hA) - 1) 闂?support.