High-contrast homogenization: Provider.Recurrence.SchattenSpectral

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

The spectral form of the Schatten trace

The mixed norm ‖·‖_{L^Q(S_Q)} of the fixed-grid section is built on the Schatten size |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q}, whose inner power is taken by the continuous functional calculus. Every estimate the section makes on that size passes through one identity: the trace of a function of a symmetric matrix is that function summed over the eigenvalues. The identity is the spectral theorem plus the invariance of the trace under conjugation by the eigenvector unitary, and it is proved here.

Two consequences are recorded because the fixed-grid proofs use them directly. The first is that the Schatten size is a nonnegative real, so it may be compared with the extended-real moments without a case split. The second is the opening display of the positive-gap estimate l.fixed.geometry.positive.gap: for a positive semidefinite D bounded above by t in the Loewner order, tr(D^Q) ≤ t^{Q-1} tr D, since every eigenvalue lies in [0, t] and the scalar inequality μ^Q ≤ t^{Q-1} μ holds there.

The trace of a function of a symmetric matrix

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_eq_sum_eigenvalues {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (f : ℝ → ℝ) : (cfc f A).trace = ∑ i : n, f (hA.eigenvalues i)

The trace of a continuous function of a symmetric matrix is the function summed over the eigenvalues. The functional calculus is realized as the conjugation of a diagonal matrix by the eigenvector unitary, and the trace does not see that conjugation.

Eigenvalue bounds from the Loewner order

theorem HCPolySupport.HighContrast.Recurrence.eigenvalues_le_of_le_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {t : ℝ} (h : A ≤ t • 1) (i : n) : hA.eigenvalues i ≤ t

A Loewner bound above is a bound on every eigenvalue: the quadratic form of t I - A at the i-th unit eigenvector is t - eigenvalues A i.

theorem HCPolySupport.HighContrast.Recurrence.le_trace_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) : A ≤ A.trace • 1

A positive semidefinite matrix is bounded above by its own trace: every eigenvalue is at most the sum of them all.

Nonnegativity of the Schatten trace

theorem HCPolySupport.HighContrast.Recurrence.zero_le_trace_cfc_rpow {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) (Q : ℝ) : 0 ≤ (cfc (fun (x : ℝ) => x ^ Q) A).trace

The Schatten trace of a symmetric matrix at a nonnegative exponent is nonnegative: the eigenvalues of A² are nonnegative and the real power of a nonnegative real is nonnegative.

The trace-power estimate of the positive-gap lemma

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_le_mul_trace {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {t Q : ℝ} (h : A ≤ t • 1) (hQ : 1 ≤ Q) : (cfc (fun (x : ℝ) => x ^ Q) A).trace ≤ t ^ (Q - 1) * A.trace

The opening display of l.fixed.geometry.positive.gap. A positive semidefinite D bounded above by t in the Loewner order satisfies tr(D^Q) ≤ t^{Q-1} tr D: every eigenvalue lies in [0, t], and there μ^Q = μ^{Q-1} μ ≤ t^{Q-1} μ.

The Schatten argument in the exponent of the reference text

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_mul_self {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {Q : ℝ} (hQ : 0 < Q) : (cfc (fun (x : ℝ) => x ^ (Q / 2)) (A * A)).trace = (cfc (fun (x : ℝ) => x ^ Q) A).trace

The Schatten size squares the matrix before taking the power Q/2. On positive semidefinite data the two operations collapse: the spectrum is nonnegative, so (x²)^{Q/2} = x^Q there, and the functional calculus composes. This is what identifies the Schatten trace of D with tr(D^Q).

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_mul_self_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {t Q : ℝ} (h : A ≤ t • 1) (hQ : 1 ≤ Q) : (cfc (fun (x : ℝ) => x ^ (Q / 2)) (A * A)).trace ≤ t ^ (Q - 1) * A.trace

The trace-power estimate in the Schatten dialect of the fixed-grid section. This is tr(D^Q) ≤ |G_hat|^{Q-1} tr D with the left side written as the Schatten trace of the squared matrix, the form in which the mixed norm reads it.

The Schatten size of a doubled block

theorem HCPolySupport.HighContrast.Recurrence.zero_le_schattenNorm {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) (Q : ℝ) : 0 ≤ schattenNorm Q H

The Schatten trace of a symmetric doubled block is nonnegative, so its Schatten size is a nonnegative real.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_rpow {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 0 < Q) : schattenNorm Q H ^ Q = (cfc (fun (x : ℝ) => x ^ (Q / 2)) (toFullBlockMat H * toFullBlockMat H)).trace

The Schatten size raised to the power Q recovers the Schatten trace: the definition takes the Q-th root of a nonnegative real.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_rpow_le_of_le_smul_one {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) (hpos : Matrix.PosSemidef (toFullBlockMat H)) {t Q : ℝ} (h : toFullBlockMat H ≤ t • 1) (hQ : 1 ≤ Q) : schattenNorm Q H ^ Q ≤ t ^ (Q - 1) * blockTrace H

The opening display of l.fixed.geometry.positive.gap in the doubled block dialect. For a positive doubled block bounded above by t in the Loewner order, the Schatten trace tr(D^Q) is at most t^{Q-1} times the block trace.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_le_blockTrace {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) (hpos : Matrix.PosSemidef (toFullBlockMat H)) {Q : ℝ} (hQ : 1 ≤ Q) : schattenNorm Q H ≤ blockTrace H

The trace bound on the Schatten size of a positive block, the step |B|_{S_Q} ≤ tr B of l.fixed.geometry.positive.gap. Applying the trace-power estimate at t = tr B gives |B|_{S_Q}^Q ≤ (tr B)^Q, and the Q-th root is monotone.