High-contrast homogenization: Provider.PortableHistory.TraceGap

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The trace gap of a relative mean under a change of normalization

p.fixed.geometry.one.grid.propagation records the effect of changing the terminal normalization on the nonlinear history. For scales j ≤ s ≤ t the relative means satisfy P_{j,t} = R^t P_{j,s} R with R^t R = P_{s,t}, and the printed step is

1 + tr(P_{j,t} - I) ≤ (1 + tr(P_{j,s} - I))(1 + tr(P_{s,t} - I)),

obtained from "cyclicity and positivity of the trace". The two ingredients are proved here at the level of an arbitrary square matrix.

Positivity of the trace of a product. For positive semidefinite X and B, tr(XB) ≥ 0: writing X = X^{1/2}X^{1/2} and using cyclicity turns the product into the congruence X^{1/2}BX^{1/2}, which is positive semidefinite. Applied to B = ‖M‖I - M it gives the comparison tr(XM) ≤ ‖M‖tr(X).

The spectral size of the congruence. The conjugation X ↦ R^t X R is controlled by ‖RR^t‖, which is ‖R‖² and hence equals ‖R^tR‖; the printed step reads that norm off the Loewner bound R^tR ≤ (1 + tr(P_{s,t} - I))I, which is in turn the elementary fact that a matrix above the identity has spectral size at most one plus its trace gap — its largest eigenvalue exceeds one by at most the sum of all the excesses.

A matrix above the identity: spectral size against trace gap

theorem HCPolySupport.HighContrast.PortableHistory.trace_sub_one_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (h : 1 ≤ A) : 0 ≤ (A - 1).trace

The trace gap of a matrix above the identity is the sum of the excesses of its eigenvalues, and is nonnegative.

theorem HCPolySupport.HighContrast.PortableHistory.norm_le_one_add_trace_sub_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) (h : 1 ≤ A) : ‖A‖ ≤ 1 + (A - 1).trace

The spectral size of a matrix above the identity is at most one plus its trace gap. All the eigenvalues exceed one, so the largest of them exceeds one by at most the sum of all the excesses.

Positivity and monotonicity of the trace of a product

theorem HCPolySupport.HighContrast.PortableHistory.trace_mul_nonneg {n : Type u_1} [Fintype n] {X B : Matrix n n ℝ} (hX : X.PosSemidef) (hB : B.PosSemidef) : 0 ≤ (X * B).trace

The trace of a product of two positive semidefinite matrices is nonnegative. Cyclicity turns tr(XB) into the trace of the congruence X^{1/2}BX^{1/2}.

theorem HCPolySupport.HighContrast.PortableHistory.trace_mul_le_trace_mul {n : Type u_1} [Fintype n] {X M N : Matrix n n ℝ} (hX : X.PosSemidef) (h : M ≤ N) : (X * M).trace ≤ (X * N).trace

The trace against a positive semidefinite matrix is monotone.

theorem HCPolySupport.HighContrast.PortableHistory.trace_mul_le_norm_mul_trace {n : Type u_1} [Fintype n] [DecidableEq n] {X M : Matrix n n ℝ} (hX : X.PosSemidef) (hM : M.PosSemidef) : (X * M).trace ≤ ‖M‖ * X.trace

The trace against a positive semidefinite matrix is bounded by its spectral size.

The congruence step

theorem HCPolySupport.HighContrast.PortableHistory.norm_mul_transpose_eq {n : Type u_1} [Fintype n] [DecidableEq n] (C : Matrix n n ℝ) : ‖C * C.transpose‖ = ‖C.transpose * C‖

The spectral size of CC^t equals the spectral size of C^tC: both are the square of the spectral size of C.

theorem HCPolySupport.HighContrast.PortableHistory.trace_conj_le {n : Type u_1} [Fintype n] [DecidableEq n] {X C : Matrix n n ℝ} (hX : X.PosSemidef) {c : ℝ} (hc : 0 ≤ c) (h : C.transpose * C ≤ c • 1) : (C.transpose * X * C).trace ≤ c * X.trace

The congruence step of p.fixed.geometry.one.grid.propagation. If the congruence C^tC is bounded by c in the Loewner order, then conjugating a positive semidefinite matrix by C multiplies its trace by at most c.

The change of terminal normalization

theorem HCPolySupport.HighContrast.PortableHistory.one_add_trace_normalize_le {n : Type u_1} [Fintype n] [DecidableEq n] {Ej Es Et : Matrix n n ℝ} (hEs : Es.PosDef) (hEt : Et.PosDef) (hsj : Es ≤ Ej) (hts : Et ≤ Es) : 1 + (matSqrt Et⁻¹ * Ej * matSqrt Et⁻¹ - 1).trace ≤ (1 + (matSqrt Es⁻¹ * Ej * matSqrt Es⁻¹ - 1).trace) * (1 + (matSqrt Et⁻¹ * Es * matSqrt Et⁻¹ - 1).trace)

The trace step of p.fixed.geometry.one.grid.propagation. For an ordered triple E_t ≤ E_s ≤ E_j of positive definite matrices, the relative mean of E_j over E_t is the congruence of the relative mean of E_j over E_s by R = E_s^{1/2}E_t^{-1/2}, whose own congruence R^tR is the relative mean of E_s over E_t; cyclicity and positivity of the trace then give the printed bound on the trace gap.