High-contrast homogenization: Provider.Response.RowPairingAnnealed

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

The cell pairing of a cutoff-defect mean row

Pairing a coarse-grained cell average against a fixed load is a Cauchy-Schwarz step for the starred coarse block: the energy map bounds the starred quadratic form of the cell average by the cell energy, and the load contributes the quadratic form of the starred inverse. The starred inverse is the reflection of the response block, so the load's contribution is read off the response block's opposite diagonal entry -- the gradient slot pairs with the lower-right block and the flux slot with the upper-left block.

Symmetry of the starred coarse block

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_coarseStarredBlockMatrix {d : ℕ} {U : Book.Ch02.Domain d} (c : Book.Ch02.CoeffOn U) : IsSymmetricBlockMat (Book.Ch02.coarseStarredBlockMatrix U c)

The starred coarse block is symmetric. Its inverse is the reflection of the response block, reflection preserves block symmetry, and matrix inversion preserves symmetry.

Pairing against an inverse block form

theorem HCPolySupport.HighContrast.Response.abs_blockVecDot_le_sqrt_mul_sqrt_of_inverse {d : ℕ} {S Sinv : BlockMat d} (hS : IsSymmetricBlockMat S) (hSpsd : ∀ (Z : BlockVec d), 0 ≤ blockVecDot Z (blockMatVecMul S Z)) (hleft : Book.Ch02.blockMatMul S Sinv = Book.Ch02.blockIdentity d) (y Qh : BlockVec d) : |blockVecDot y Qh| ≤ √(blockVecDot y (blockMatVecMul S y)) * √(blockVecDot Qh (blockMatVecMul Sinv Qh))

Pairing against an inverse block form. For a symmetric positive semidefinite block form with a right inverse, the plain pairing is bounded by the form's quadratic mean of the first vector and the inverse form's quadratic mean of the second.

The two diagonal Schur loads as quadratic forms

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadFlux_eq {d : ℕ} {H : BlockMat d} (hpsd : Matrix.PosSemidef H.lowerRight) (hdet : IsUnit (Matrix.det H.lowerRight)) (Qcen : Vec d) : profileSchurLoadFlux H Qcen ^ 2 = vecDot Qcen (matVecMul H.lowerRight Qcen)

The flux half of the Schur load is the lower-right quadratic form.

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadGradient_eq {d : ℕ} {H : BlockMat d} (hpsd : Matrix.PosSemidef H.upperLeft) (Pcen : Vec d) : profileSchurLoadGradient H Pcen ^ 2 = vecDot Pcen (matVecMul H.upperLeft Pcen)

The gradient half of the Schur load is the upper-left quadratic form.

The per-cell pairing through the starred bridge

theorem HCPolySupport.HighContrast.Response.abs_vecDot_averageVec_potential_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (c : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier c.toCoeffField) (hpsd : Matrix.PosSemidef (Book.Ch02.coarseBlockMatrix U c).lowerRight) (hdet : IsUnit (Matrix.det (Book.Ch02.coarseBlockMatrix U c).lowerRight)) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U c Y) (Qcen : Vec d) : |vecDot Qcen (Book.Ch02.averageVec U Y.potential)| ≤ √(Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField c x) (Y.eval x))) * profileSchurLoadFlux (Book.Ch02.coarseBlockMatrix U c) Qcen

The gradient-slot cell pairing. The potential average of a doubled response field pairs with a load through the cell energy and the flux half of the Schur load of the cell's response block.

theorem HCPolySupport.HighContrast.Response.abs_vecDot_averageVec_flux_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (c : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier c.toCoeffField) (hpsd : Matrix.PosSemidef (Book.Ch02.coarseBlockMatrix U c).upperLeft) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U c Y) (Pcen : Vec d) : |vecDot Pcen (Book.Ch02.averageVec U Y.flux)| ≤ √(Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField c x) (Y.eval x))) * profileSchurLoadGradient (Book.Ch02.coarseBlockMatrix U c) Pcen

The flux-slot cell pairing. The flux average of a doubled response field pairs with a load through the cell energy and the gradient half of the Schur load of the cell's response block.

The annealed Schur loads

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadFlux_hatted_eq_blockQuadratic {d : ℕ} (h : Mat d) (H : BlockMat d) (hpsd : Matrix.PosSemidef (profileHattedBlock h H).lowerRight) (hdet : IsUnit (Matrix.det (profileHattedBlock h H).lowerRight)) (Qcen : Vec d) : profileSchurLoadFlux (profileHattedBlock h H) Qcen ^ 2 = blockVecDot (0, Qcen) (blockMatVecMul H (0, Qcen))

The flux half of the Schur load of a hatted block is the block's own lower-right quadratic form: the hatting shear only shifts the flux slot by a multiple of the potential slot, which vanishes here.

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadGradient_hatted_eq_blockQuadratic {d : ℕ} (h : Mat d) (H : BlockMat d) (hpsd : Matrix.PosSemidef (profileHattedBlock h H).upperLeft) (Pcen : Vec d) : profileSchurLoadGradient (profileHattedBlock h H) Pcen ^ 2 = blockVecDot (Pcen, matVecMul h Pcen) (blockMatVecMul H (Pcen, matVecMul h Pcen))

The gradient half of the Schur load of a hatted block is the block's quadratic form at the sheared potential load.

theorem HCPolySupport.HighContrast.Response.integral_sq_profileSchurLoadFlux_hatted_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (h : Mat d) (Qcen : Vec d) (hpsdA : Matrix.PosSemidef (profileHattedBlock h (annealedBlock P U)).lowerRight) (hdetA : IsUnit (Matrix.det (profileHattedBlock h (annealedBlock P U)).lowerRight)) (hpsd : ∀ (a : CoeffSpace d), Matrix.PosSemidef (profileHattedBlock h (coarseBlock U a)).lowerRight) (hdet : ∀ (a : CoeffSpace d), IsUnit (Matrix.det (profileHattedBlock h (coarseBlock U a)).lowerRight)) : profileSchurLoadFlux (profileHattedBlock h (annealedBlock P U)) Qcen ^ 2 = ∫ (a : CoeffSpace d), profileSchurLoadFlux (profileHattedBlock h (coarseBlock U a)) Qcen ^ 2 ∂P

The annealed flux load is the expectation of the pathwise flux load. The lower-right quadratic form is linear in the block, so the annealed Schur coordinate is the coordinate of the full annealed matrix.

theorem HCPolySupport.HighContrast.Response.integral_sq_profileSchurLoadGradient_hatted_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (h : Mat d) (Pcen : Vec d) (hpsdA : Matrix.PosSemidef (profileHattedBlock h (annealedBlock P U)).upperLeft) (hpsd : ∀ (a : CoeffSpace d), Matrix.PosSemidef (profileHattedBlock h (coarseBlock U a)).upperLeft) : profileSchurLoadGradient (profileHattedBlock h (annealedBlock P U)) Pcen ^ 2 = ∫ (a : CoeffSpace d), profileSchurLoadGradient (profileHattedBlock h (coarseBlock U a)) Pcen ^ 2 ∂P

The annealed gradient load is the expectation of the pathwise gradient load.

The scale-sum premise of the row closers