Coarse-graining support: Support.Book.Ch02.Theorems.BlockCoarseMatrixDefinitions #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Public theorem package for l.block.coarse.matrices.basic.definitions.
This is the block-matrix surface that connects the doubled formalism back to
the scalar coarse matrices without exposing legacy coarse-data witnesses. The
canonical public theorem proving this package is blockCoarseMatrixTheory in
BlockCoarseMatrix.lean.
- doubled_response_splitting (P Q : BlockVec d) : doubledResponseJ U a P Q = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P) + 1 / 2 * blockVecDot Q (blockMatVecMul (coarseStarredBlockMatrixInv U a) Q) - blockVecDot P Q
- block_matrix_posDef : BlockPosDef (coarseBlockMatrix U a)
- starred_matrix_posDef : BlockPosDef (coarseStarredBlockMatrix U a)
- starred_inverse_posDef : BlockPosDef (coarseStarredBlockMatrixInv U a)
- starred_left_inverse : blockMatMul (coarseStarredBlockMatrix U a) (coarseStarredBlockMatrixInv U a) = blockIdentity d
- starred_right_inverse : blockMatMul (coarseStarredBlockMatrixInv U a) (coarseStarredBlockMatrix U a) = blockIdentity d
- block_matrix_subadditive (P : DomainPartition U) (aCell : (i : P.Cell) → CoeffOn (P.cell i)) : (∀ (i : P.Cell), a.RestrictsTo (aCell i)) → BlockMatLoewnerLE (coarseBlockMatrix U a) (P.weightedBlockAverage fun (i : P.Cell) => coarseBlockMatrix (P.cell i) (aCell i))
- starred_inverse_subadditive (P : DomainPartition U) (aCell : (i : P.Cell) → CoeffOn (P.cell i)) : (∀ (i : P.Cell), a.RestrictsTo (aCell i)) → BlockMatLoewnerLE (coarseStarredBlockMatrixInv U a) (P.weightedBlockAverage fun (i : P.Cell) => coarseStarredBlockMatrixInv (P.cell i) (aCell i))