Coarse-graining support: Support.Book.Ch02.Theorems.BlockMatrixFieldDefinitions #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
structure
HCPolySupport.Book.Ch02.BlockMatrixFieldAlgebraTheory
{d : ℕ}
(U : Domain d)
(a : CoeffOn U)
:
Public theorem package for l.block.matrix.field.basic.definitions.
All coefficient-field conclusions are a.e. on the Chapter 2 domain, preserving
the public a.e.-native coefficient interface. The canonical public theorem
proving this package is blockMatrixFieldAlgebraTheory in
BlockMatrixField.lean.
- field_symmetric : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, IsSymmetricBlockMat (blockMatrixField a x)
- field_posDef : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, BlockPosDef (blockMatrixField a x)
- factorization : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, blockMatrixField a x = blockMatMul (blockMatTranspose (blockG (-skewPart (a.toCoeffField x)))) (blockMatMul (blockDiag (symmPart (a.toCoeffField x)) (symmPart (a.toCoeffField x))⁻¹) (blockG (-skewPart (a.toCoeffField x))))
- inverse_formula : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, blockMatrixInverseField a x = blockReflect (blockMatrixField a x)
- energy_density : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, ∀ (X : BlockVec d), blockEnergyDensityAt a X x = 1 / 2 * blockVecDot X (blockMatVecMul (blockMatrixField a x) X)