Coarse-graining support: Support.CoarseGraining.SharpBlockBounds.Basic

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

Pointwise block algebra (items A4–A9)

Sharp-constant pointwise block-matrix algebra of Proposition 2.1 of the high-moment paper (Armstrong–Kuusi–Loher, to appear). Items A4–A8-upper live here; the diagonal-sandwich lower bound A8 and the two-field comparison A9 (which need the block Fenchel/inverse machinery) live in SharpBlockBounds/DiagonalSandwich.lean.

Notation throughout: A : Mat d, s := symmPart A, k := skewPart A, and bfA := blockMatrixOfCoeff A is the doubled block matrix [[s + kᵀ s⁻¹ k, −kᵀ s⁻¹], [−s⁻¹ k, s⁻¹]].

Elementary matrix/vector helpers

theorem HCPolySupport.zero_matVecMul {d : ℕ} (x : Vec d) : matVecMul 0 x = 0

The zero matrix annihilates every vector.

theorem HCPolySupport.matVecMul_eq_symmPart_add_skewPart {d : ℕ} (A : Mat d) (w : Vec d) : matVecMul A w = matVecMul (symmPart A) w + matVecMul (skewPart A) w

A = symmPart A + skewPart A at the level of the vector action.

A7 — the block quadratic identity

(p,q) · bfA (p,q) = p · s p + (q − k p) · s⁻¹ (q − k p). This is the identity blockMatrixOfCoeff_quadratic_eq, re-exported under the item-A7 name.

theorem HCPolySupport.blockMatrixOfCoeff_quadratic {d : ℕ} (A : Mat d) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) = vecDot p (matVecMul (symmPart A) p) + vecDot (q - matVecMul (skewPart A) p) (matVecMul (symmPart A)⁻¹ (q - matVecMul (skewPart A) p))

A7. The doubled quadratic form of bfA in Schur-complement form.

The image identity and the sharp flux/coercivity bound

s + kᵀ s⁻¹ k is the quadratic form w ↦ (A w) · s⁻¹ (A w); combined with the flux inequality (★) this gives the sharp nonsymmetric coercivity A4.

theorem HCPolySupport.image_symmPartInv_quadratic_eq {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (w : Vec d) : vecDot w (matVecMul (symmPart A) w) + vecDot (matVecMul (skewPart A) w) (matVecMul (symmPart A)⁻¹ (matVecMul (skewPart A) w)) = vecDot (matVecMul A w) (matVecMul (symmPart A)⁻¹ (matVecMul A w))

Quadratic-form identity w · s w + (k w) · s⁻¹ (k w) = (A w) · s⁻¹ (A w).

theorem HCPolySupport.image_symmPartInv_le {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (w : Vec d) : vecDot (matVecMul A w) (matVecMul (symmPart A)⁻¹ (matVecMul A w)) ≤ Lam * vecNormSq w

The sharp flux/coercivity bound (A w) · s⁻¹ (A w) ≤ Lam · ‖w‖², proved by Cauchy–Schwarz against the flux inequality (★) for Aᵀ.

theorem HCPolySupport.skew_symmPartInv_le {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (w : Vec d) : vecDot (matVecMul (skewPart A) w) (matVecMul (symmPart A)⁻¹ (matVecMul (skewPart A) w)) ≤ Lam * vecNormSq w - vecDot w (matVecMul (symmPart A) w)

The skew Schur term is controlled by A4's budget: (k w) · s⁻¹ (k w) ≤ Lam ‖w‖² − w · s w.

A4 — nonsymmetric coercivity

theorem HCPolySupport.upperLeft_matLoewnerLE_smul_one_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) : MatLoewnerLE (symmPart A + matTranspose (skewPart A) * (symmPart A)⁻¹ * skewPart A) (Θ • 1)

A4. s + kᵀ s⁻¹ k ≤ Θ • 1 in the Loewner order.

A5 — sharp flux bounds

theorem HCPolySupport.vecDot_matVecMul_transpose_mul_self {d : ℕ} (A : Mat d) (x : Vec d) : vecDot x (matVecMul (matTranspose A * A) x) = vecNormSq (matVecMul A x)

Quadratic form of Aᵀ A is the squared image norm ‖A x‖².

theorem HCPolySupport.vecDot_matVecMul_self_mul_transpose {d : ℕ} (A : Mat d) (x : Vec d) : vecDot x (matVecMul (A * matTranspose A) x) = vecNormSq (matVecMul (matTranspose A) x)

Quadratic form of A Aᵀ is the squared adjoint image norm ‖Aᵀ x‖².

theorem HCPolySupport.transpose_mul_self_matLoewnerLE_smul_symmPart_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) : MatLoewnerLE (matTranspose A * A) (Θ • symmPart A)

A5a. Aᵀ A ≤ Θ • s in the Loewner order.

theorem HCPolySupport.self_mul_transpose_matLoewnerLE_smul_symmPart_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) : MatLoewnerLE (A * matTranspose A) (Θ • symmPart A)

A5b. A Aᵀ ≤ Θ • s in the Loewner order.

theorem HCPolySupport.vecNormSq_image_add_transpose_le_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (e : Vec d) : vecNormSq (matVecMul A e) + vecNormSq (matVecMul (matTranspose A) e) ≤ 2 * Θ * vecDot e (matVecMul (symmPart A) e)

A5 (corollary). ‖A e‖² + ‖Aᵀ e‖² ≤ 2 Θ (e · s e).

A6 — skew bound

theorem HCPolySupport.vecNormSq_matVecMul_skewPart_le_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (e : Vec d) : vecNormSq (matVecMul (skewPart A) e) ≤ Θ ^ 2 * vecNormSq e

A6. ‖k e‖² ≤ Θ² ‖e‖².

A8 (upper) — diagonal sandwich, upper half

theorem HCPolySupport.blockVecDot_blockMatVecMul_blockDiag_smul_one {d : ℕ} (a b : ℝ) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (Book.Ch02.blockDiag (a • 1) (b • 1)) (p, q)) = a * vecNormSq p + b * vecNormSq q

A block-diagonal matrix with scalar-multiple-of-identity blocks acts diagonally on doubled vectors.

theorem HCPolySupport.vecDot_matVecMul_sub_le_two {d : ℕ} {N : Mat d} (hN : ∀ (x : Vec d), 0 ≤ vecDot x (matVecMul N x)) (a b : Vec d) : vecDot (a - b) (matVecMul N (a - b)) ≤ 2 * (vecDot a (matVecMul N a) + vecDot b (matVecMul N b))

Cauchy-type parallelogram bound for a p.s.d. quadratic form: (a − b) · N (a − b) ≤ 2 (a · N a + b · N b).

theorem HCPolySupport.blockMatrixOfCoeff_blockMatLoewnerLE_blockDiag_of_isThetaElliptic {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) : BlockMatLoewnerLE (blockMatrixOfCoeff A) (Book.Ch02.blockDiag ((2 * Θ) • 1) (2 • 1))

A8 (upper). bfA ≤ blockDiag (2Θ • 1) (2 • 1) in the block Loewner order.