High-contrast homogenization: Provider.Recurrence.SchattenEntries

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

Entries, traces and the Schatten size

The scalarization of the fixed-grid estimates rests on three comparisons between the Schatten size |H|_{S_Q} of a symmetric doubled block and the scalar data of its entries.

The entrywise bound |H_{ab}| ≤ |H|_{S_Q} is the step that turns a matrix estimate into 4d² scalar estimates in l.fixed.geometry.matrix.averaging. Its content is that a single entry of a symmetric matrix is dominated by the largest eigenvalue in absolute value, which in turn is dominated by the ℓ^Q-size of the whole spectrum.

The Hilbert–Schmidt comparison |H|_{S_Q} ≤ (Σ_{a,b} H_{ab}²)^{1/2} for Q ≥ 2 is the first half of the scalarization display of the same lemma. It is the ℓ^Q ⊆ ℓ^2 embedding on the spectrum, read through the identity Σ_i λ_i² = tr(H²) = Σ_{a,b} H_{ab}².

The trace comparison tr D ≤ m^{1-1/Q}|D|_{S_Q} for D ≥ 0 is the step of l.fixed.geometry.positive.gap that converts the trace produced by the positivity argument into the Schatten size the conclusion is stated in. It is Hölder's inequality against the constant function on the m eigenvalues; here m = 2d is the size of a doubled block.

The Schatten trace of a symmetric matrix

theorem HCPolySupport.HighContrast.Recurrence.trace_cfc_rpow_mul_self_eq_sum_abs_rpow {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 spectral form of the Schatten trace. The Schatten size squares its argument before applying the power Q/2; on the spectrum this composition is (x²)^{Q/2} = |x|^Q, so the trace it takes is the ℓ^Q-sum of the eigenvalues in absolute value. No positivity is needed: the absolute value is what the squaring leaves behind.

The entrywise bound

theorem HCPolySupport.HighContrast.Recurrence.abs_apply_le_of_abs_eigenvalues_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) {t : ℝ} (ht : 0 ≤ t) (h : ∀ (i : n), |hA.eigenvalues i| ≤ t) (α β : n) : |A α β| ≤ t

A spectral bound is an entrywise bound. Every entry of a symmetric matrix is bounded by any bound on the absolute values of its eigenvalues.

The Hilbert–Schmidt trace

theorem HCPolySupport.HighContrast.Recurrence.trace_mul_self_eq_sum_sq {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.IsHermitian) : (A * A).trace = ∑ α : n, ∑ β : n, A α β ^ 2

The trace of the square of a symmetric matrix is the sum of the squares of its entries: this is the Hilbert–Schmidt norm in the two forms the scalarization display compares.

The trace–Schatten comparison

theorem HCPolySupport.HighContrast.Recurrence.trace_le_card_rpow_mul_rpow_trace_cfc_rpow {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A : Matrix n n ℝ} (hA : A.PosSemidef) {Q : ℝ} (hQ : 1 ≤ Q) : A.trace ≤ ↑(Fintype.card n) ^ (1 - Q⁻¹) * (cfc (fun (x : ℝ) => x ^ Q) A).trace ^ Q⁻¹

The trace comparison of l.fixed.geometry.positive.gap at the level of a general positive semidefinite matrix: tr D ≤ m^{1-1/Q}(tr(D^Q))^{1/Q}.

The three comparisons for a doubled block

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

The Schatten size of a symmetric doubled block is the ℓ^Q-size of its spectrum.

theorem HCPolySupport.HighContrast.Recurrence.abs_toFullBlockMat_le_schattenNorm {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 0 < Q) (α β : BlockCoord d) : |toFullBlockMat H α β| ≤ schattenNorm Q H

The entrywise bound |H_{ab}| ≤ |H|_{S_Q} of l.fixed.geometry.matrix.averaging. Each eigenvalue is dominated by the ℓ^Q-size of the spectrum, and a spectral bound is an entrywise bound.

theorem HCPolySupport.HighContrast.Recurrence.schattenNorm_le_sum_sq_rpow {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) {Q : ℝ} (hQ : 2 ≤ Q) : schattenNorm Q H ≤ (∑ α : BlockCoord d, ∑ β : BlockCoord d, toFullBlockMat H α β ^ 2) ^ 2⁻¹

The Hilbert–Schmidt comparison |H|_{S_Q} ≤ (Σ_{a,b}H_{ab}²)^{1/2} for Q ≥ 2, the matrix half of the scalarization display of l.fixed.geometry.matrix.averaging. The trace-power estimate applied to H² at the exponent Q/2 gives tr((H²)^{Q/2}) ≤ (tr H²)^{Q/2}, and tr H² = Σ_{a,b}H_{ab}².

theorem HCPolySupport.HighContrast.Recurrence.blockTrace_le_card_rpow_mul_schattenNorm {d : ℕ} {H : BlockMat d} (hd : 0 < d) (hpos : Matrix.PosSemidef (toFullBlockMat H)) {Q : ℝ} (hQ : 1 ≤ Q) : blockTrace H ≤ (2 * ↑d) ^ (1 - Q⁻¹) * schattenNorm Q H

The trace comparison tr D ≤ m^{1-1/Q}|D|_{S_Q} of l.fixed.geometry.positive.gap, for a positive doubled block: the matrix size m of a doubled block is 2d, and the hypothesis 0 < d is the lemma's m ≥ 1.