High-contrast homogenization: Provider.Recurrence.SchattenSandwich

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

The Schatten size and the scalar Loewner sandwich

The fixed-grid section measures a symmetric doubled block by the Schatten size |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q}. Squaring folds the sign away — for every real x one has (x²)^{Q/2} = |x|^Q — so the Schatten trace of a symmetric matrix is Σ|λ_i|^Q, its absolute eigenvalues raised to the Q-th power and summed. That identity is proved first, with no positivity hypothesis, and everything else in this file reads off it.

What the identity gives is a two-sided comparison between the Schatten size and the scalar Loewner sandwich -tI ≤ H ≤ tI. In one direction a single term of a sum of nonnegative terms is at most the whole, so |λ_i| ≤ |H|_{S_Q} for every i and H is caught between ∓|H|_{S_Q}I. In the other, 2d terms each at most t^Q sum to at most 2d·t^Q, so a block caught between ∓tI has Schatten size at most (2d)^{1/Q}t. The dimensional factor is the whole gap between the two directions, and the fixed-grid constants absorb it.

The passage between an eigenvalue bound and a Loewner bound runs both ways through the spectral theorem: the quadratic form of tI ∓ H at the i-th unit eigenvector is t ∓ λ_i, and conversely tI ∓ H is the conjugate of the diagonal matrix t ∓ diag(λ) by the eigenvector unitary.

The Schatten trace of a symmetric matrix

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_mul_self_eq_sum_abs {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {Q : ℝ} (hQ : 0 < Q) : (cfc (fun (x : ℝ) => x ^ (Q / 2)) (A * A)).trace = ∑ i : n, |hA.eigenvalues i| ^ Q

The Schatten trace is the sum of the Q-th powers of the absolute eigenvalues. Squaring folds the sign away: (x²)^{Q/2} = |x|^Q for every real x, so no positivity hypothesis is needed on the matrix.

Eigenvalues and the scalar Loewner sandwich

theorem HCPolySupport.HighContrast.Recurrence.abs_eigenvalues_le_of_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {t : ℝ} (hsub : (t • 1 - A).PosSemidef) (hadd : (t • 1 + A).PosSemidef) (i : n) : |hA.eigenvalues i| ≤ t

A two-sided scalar bound bounds every eigenvalue in absolute value. The quadratic forms of t I - A and t I + A at the i-th unit eigenvector are t - λ_i and t + λ_i.

theorem HCPolySupport.HighContrast.Recurrence.posSemidef_smul_one_sub_add_of_abs_eigenvalues_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {t : ℝ} (h : ∀ (i : n), |hA.eigenvalues i| ≤ t) : (t • 1 - A).PosSemidef ∧ (t • 1 + A).PosSemidef

A bound on the absolute eigenvalues is a two-sided scalar bound. This is the spectral theorem read as a congruence: the diagonal matrices t I ∓ diag(eigenvalues) have nonnegative entries.

The Schatten size of a doubled block

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_rpow_eq_sum_abs {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 0 < Q) : schattenNorm Q H ^ Q = ∑ i : BlockCoord d, |⋯.eigenvalues i| ^ Q

The Schatten trace of a symmetric doubled block is the sum of the Q-th powers of the absolute eigenvalues of its flattening.

theorem HCPolySupport.HighContrast.Recurrence.abs_eigenvalues_le_schattenNorm {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 0 < Q) (i : BlockCoord d) : |⋯.eigenvalues i| ≤ schattenNorm Q H

The Schatten size dominates every eigenvalue in absolute value: one term of a sum of nonnegative terms is at most the whole.

theorem HCPolySupport.HighContrast.Recurrence.posSemidef_schattenNorm_smul_one_sub_add {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 0 < Q) : Matrix.PosSemidef (schattenNorm Q H • 1 - toFullBlockMat H) ∧ Matrix.PosSemidef (schattenNorm Q H • 1 + toFullBlockMat H)

A symmetric block is caught between ∓|H|_{S_Q}I in the Loewner order.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_le_of_posSemidef {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {t Q : ℝ} (hQ : 0 < Q) (ht : 0 ≤ t) (hsub : Matrix.PosSemidef (t • 1 - toFullBlockMat H)) (hadd : Matrix.PosSemidef (t • 1 + toFullBlockMat H)) : schattenNorm Q H ≤ (2 * ↑d) ^ Q⁻¹ * t

A symmetric block caught between ∓tI has Schatten size at most (2d)^{1/Q}t: each of the 2d absolute eigenvalues is at most t.