Coarse-graining support: Support.CoarseGraining.QuadraticStability.CauchySchwarz

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Quadratic stability, items B′1 and B′2

Pure-algebra half of Lemma 4.1 (l.quadratic.stability) of the high-moment paper (Armstrong–Kuusi–Loher, to appear). This file proves the two pointwise (matrix-level) inequalities, phrased entirely through blockVecDot/blockMatVecMul on BlockVec d/BlockMat d:

• B′1 (abs_blockVecDot_blockMatVecMul_le_of_isSymmetricBlockMat): Cauchy– Schwarz for a symmetric positive semidefinite block form, proved by the discriminant argument on t ↦ (X + t•Y)·B(X + t•Y) — no matrix square roots.
• B′2 (abs_blockVecDot_sub_le_of_blockMatLoewnerLE): the mixed-metric inequality, from the triangle inequality, B′1 on each of the two forms, and the two Loewner hypotheses.

No EuclideanSpace.

B′1 — Cauchy–Schwarz for a positive semidefinite block form

theorem HCPolySupport.blockVecDot_blockMatVecMul_add_smul_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) (X Y : BlockVec d) (t : ℝ) : blockVecDot (X + t • Y) (blockMatVecMul B (X + t • Y)) = blockVecDot Y (blockMatVecMul B Y) * (t * t) + 2 * blockVecDot X (blockMatVecMul B Y) * t + blockVecDot X (blockMatVecMul B X)

The t-expansion of the quadratic form (X + t•Y)·B(X + t•Y) for a symmetric block matrix B.

theorem HCPolySupport.abs_blockVecDot_blockMatVecMul_le_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) (hpsd : ∀ (Z : BlockVec d), 0 ≤ blockVecDot Z (blockMatVecMul B Z)) (X Y : BlockVec d) : |blockVecDot X (blockMatVecMul B Y)| ≤ √(blockVecDot X (blockMatVecMul B X)) * √(blockVecDot Y (blockMatVecMul B Y))

B′1. Cauchy–Schwarz for a symmetric positive semidefinite block form: |X·BY| ≤ √(X·BX) · √(Y·BY). Proved by the discriminant of the nonnegative quadratic t ↦ (X + t•Y)·B(X + t•Y).

B′2 — the mixed-metric inequality

theorem HCPolySupport.blockVecDot_le_smul_of_blockMatLoewnerLE {d : ℕ} {B C : BlockMat d} {K : ℝ} (h : BlockMatLoewnerLE B (K • C)) (X : BlockVec d) : blockVecDot X (blockMatVecMul B X) ≤ K * blockVecDot X (blockMatVecMul C X)

Unfold BlockMatLoewnerLE B_tilde (K • B) to the plain quadratic-form comparison X·B_tildeX ≤ K·(X·BX).

theorem HCPolySupport.abs_blockVecDot_sub_le_of_blockMatLoewnerLE {d : ℕ} {B Bt : BlockMat d} {K : ℝ} (hBsymm : IsSymmetricBlockMat B) (hBtsymm : IsSymmetricBlockMat Bt) (hBpsd : ∀ (Z : BlockVec d), 0 ≤ blockVecDot Z (blockMatVecMul B Z)) (hBtpsd : ∀ (Z : BlockVec d), 0 ≤ blockVecDot Z (blockMatVecMul Bt Z)) (hK : 1 ≤ K) (hBt_le : BlockMatLoewnerLE Bt (K • B)) (hB_le : BlockMatLoewnerLE B (K • Bt)) (X Y : BlockVec d) : |blockVecDot X (blockMatVecMul Bt Y) - blockVecDot X (blockMatVecMul B Y)| ≤ 2 * √K * √(blockVecDot X (blockMatVecMul B X)) * √(blockVecDot Y (blockMatVecMul Bt Y))

B′2. The mixed-metric inequality. For symmetric positive semidefinite B, B_tilde with 1 ≤ K, B_tilde ≤ K•B and B ≤ K•B_tilde in the block Loewner order, |X·B_tildeY − X·BY| ≤ 2·√K·√(X·BX)·√(Y·B_tildeY).