High-contrast homogenization: Provider.Sharp.ReflectionOrder

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

The sharp order and the two signed reflection bounds

The primal-adjoint involution of s.scale.selection sends a doubled block H to H^♯ = R H^{-1} R, the reflection being R = (0 I; I 0), and the pathwise elementary block bounds assert H^♯ ≤ H. This file isolates the linear algebra of that assertion: on a symmetric positive definite block the sharp order is equivalent to the pair of signed reflection bounds -R ≤ H and R ≤ H, that is, to the single scalar statement that half the doubled quadratic form of H dominates the absolute pairing |P₁ · P₂| of the two halves of a doubled vector.

Both directions are elementary and use no spectral theory. The quadratic form of R at (P₁, P₂) is 2 P₁·P₂, so the two signed bounds polarize to 2 (u₁·v₂ + u₂·v₁) ≤ u·Hu + v·Hv; fed the pair u = X, v = H^{-1} R X, that inequality gives the sharp order at X, because the mixed pairing and the second quadratic term are then both equal to (RX)·H^{-1}(RX). Conversely the Young inequality 2 u·v ≤ u·Hu + v·H^{-1}v, itself the expansion of (u - H^{-1}v)·H(u - H^{-1}v) ≥ 0, evaluated at v = ±RX returns the two signed bounds.

The direction that produces the sharp order needs no invertibility: where the flattened block is singular the sharp is the zero block, and the two signed bounds already force the quadratic form of H to be nonnegative.

The reflection and the dilation as quadratic forms

theorem HCPolySupport.HighContrast.Sharp.blockVecDot_blockMatVecMul_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockScale c A) X) = c * blockVecDot X (blockMatVecMul A X)

The doubled quadratic form of a dilation is the dilated quadratic form.

theorem HCPolySupport.HighContrast.Sharp.blockMatLoewnerLE_of_dim_zero (A B : BlockMat 0) : BlockMatLoewnerLE A B

In dimension zero every doubled quadratic form vanishes, so the block Loewner order holds between any two blocks.

The structural inverse

theorem HCPolySupport.HighContrast.Sharp.blockMatMul_blockMatInv {d : ℕ} {H : BlockMat d} (hdet : IsUnit (Matrix.det (toFullBlockMat H))) : Book.Ch02.blockMatMul H (Book.Ch02.blockMatInv H) = Book.Ch02.blockIdentity d

The structural inverse is a right inverse where the flattened block is invertible.

theorem HCPolySupport.HighContrast.Sharp.blockMatVecMul_blockMatInv {d : ℕ} {H : BlockMat d} (hdet : IsUnit (Matrix.det (toFullBlockMat H))) (Y : BlockVec d) : blockMatVecMul H (blockMatVecMul (Book.Ch02.blockMatInv H) Y) = Y

The structural inverse is a right inverse of the doubled action.

theorem HCPolySupport.HighContrast.Sharp.blockVecDot_blockMatVecMul_blockSharp {d : ℕ} (H : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockSharp H) X) = blockVecDot (X.2, X.1) (blockMatVecMul (Book.Ch02.blockMatInv H) (X.2, X.1))

The sharp quadratic form is the inverse quadratic form at the swapped vector.

Polarization of the signed bounds

theorem HCPolySupport.HighContrast.Sharp.two_mul_blockVecDot_swap_le {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hplus : ∀ (X : BlockVec d), vecDot X.1 X.2 ≤ 1 / 2 * blockVecDot X (blockMatVecMul H X)) (hminus : ∀ (X : BlockVec d), -vecDot X.1 X.2 ≤ 1 / 2 * blockVecDot X (blockMatVecMul H X)) (u v : BlockVec d) : 2 * blockVecDot (u.2, u.1) v ≤ blockVecDot u (blockMatVecMul H u) + blockVecDot v (blockMatVecMul H v)

The two signed reflection bounds polarize: the mixed pairing of two doubled vectors is dominated by the sum of their quadratic forms.

The sharp order from the signed bounds

theorem HCPolySupport.HighContrast.Sharp.blockMatLoewnerLE_blockSharp_of_signed {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hplus : ∀ (X : BlockVec d), vecDot X.1 X.2 ≤ 1 / 2 * blockVecDot X (blockMatVecMul H X)) (hminus : ∀ (X : BlockVec d), -vecDot X.1 X.2 ≤ 1 / 2 * blockVecDot X (blockMatVecMul H X)) : BlockMatLoewnerLE (blockSharp H) H

The signed reflection bounds give the sharp order: this is the linear algebra behind the elementary block bounds. No invertibility is assumed.

The signed bounds from the sharp order

theorem HCPolySupport.HighContrast.Sharp.zero_le_blockVecDot_blockMatVecMul_of_blockPosDef {d : ℕ} {H : BlockMat d} (hpd : Book.Ch02.BlockPosDef H) (Z : BlockVec d) : 0 ≤ blockVecDot Z (blockMatVecMul H Z)

A positive definite doubled block has a nonnegative doubled quadratic form.