CompletedSquares

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the two completed-square formulas for the doubled response

This file proves local versions of the displays e.bfJ.magic and e.bfJ.magic2 of ABK26:

• bfJ(U,P,Q) = 1/2 P. (bfA - bfA_*) P + 1/2 (Q - bfA_* P). bfA_*^{-1} (Q - bfA_* P);
• bfJ(U,P,Q) = 1/2 Q. (bfA_*^{-1} - bfA^{-1}) Q + 1/2 (P - bfA^{-1} Q). bfA (P - bfA^{-1} Q).

Both are pure block-matrix algebra on top of CoarseGraining's public splitting

bfJ(U,P,Q) = 1/2 P . bfA P + 1/2 Q . bfA_*^{-1} Q - P . Q

(Homogenization.Book.Ch02.BlockCoarseMatrixTheory.doubled_response_splitting), using only symmetry of bfA and bfA_*^{-1} and the two-sided inverse relations between bfA_* and bfA_*^{-1}.

Notation for differences of block matrices

BlockMat d is a four-field structure without a Sub instance, so CoarseGraining writes the difference of two block matrices as ofFullBlockMat (toFullBlockMat A - toFullBlockMat B); the quadratic form of such a difference splits by Homogenization.blockVecDot_blockMatVecMul_ofFullBlockMat_sub. That is the spelling used below.

The inverse of bfA

CoarseGraining names bfA_*^{-1}(U;a) = blockReflect (bfA(U;a)) and bfA_*(U;a) = blockMatInv (bfA_*^{-1}(U;a)) but does not name bfA^{-1}. It is introduced here as coarseBlockMatrixInv, defined by the same generic block inverse blockMatInv, and identified with blockReflect (bfA_*(U;a)); the two-sided inverse identities then follow from CoarseGraining's starred_left_inverse and starred_right_inverse because blockReflect is a multiplicative involution.

Bilinearity helpers for the doubled pairing

blockReflect is a multiplicative involution

The inverse of the coarse block matrix

noncomputable def Algsuperdiff.Section3.Provider.Block.coarseBlockMatrixInv {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.BlockMat d

The inverse bfA^{-1}(U; a) of the coarse block matrix, defined by the same generic doubled inverse blockMatInv that CoarseGraining uses for bfA_*(U; a).

Equations

• Algsuperdiff.Section3.Provider.Block.coarseBlockMatrixInv U a = HCPolySupport.Book.Ch02.blockMatInv (HCPolySupport.Book.Ch02.coarseBlockMatrix U a)

theorem Algsuperdiff.Section3.Provider.Block.coarseBlockMatrixInv_eq_blockReflect {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : coarseBlockMatrixInv U a = HCPolySupport.blockReflect (HCPolySupport.Book.Ch02.coarseStarredBlockMatrix U a)

bfA^{-1}(U; a) is the block reflection of bfA_*(U; a), mirroring CoarseGraining's identity bfA_*^{-1}(U; a) = blockReflect (bfA(U; a)).

theorem Algsuperdiff.Section3.Provider.Block.blockMatVecMul_coarseBlockMatrix_coarseBlockMatrixInv {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (HCPolySupport.blockMatVecMul (coarseBlockMatrixInv U a) X) = X

bfA(U; a) cancels bfA^{-1}(U; a) on doubled loads.

e.bfJ.magic2: completing the square in the potential variable

theorem Algsuperdiff.Section3.Provider.Block.doubledResponseJ_eq_primal_completed_square {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (P Q : HCPolySupport.BlockVec d) : HCPolySupport.Book.Ch02.doubledResponseJ U a P Q = 1 / 2 * HCPolySupport.blockVecDot Q (HCPolySupport.blockMatVecMul (HCPolySupport.ofFullBlockMat (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.coarseStarredBlockMatrixInv U a) - HCPolySupport.toFullBlockMat (coarseBlockMatrixInv U a))) Q) + 1 / 2 * HCPolySupport.blockVecDot (P - HCPolySupport.blockMatVecMul (coarseBlockMatrixInv U a) Q) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (P - HCPolySupport.blockMatVecMul (coarseBlockMatrixInv U a) Q))

Second completed-square formula e.bfJ.magic2 for the doubled response.