Coarse-graining support: Support.Book.Ch02.Block

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

def HCPolySupport.Book.Ch02.blockMatTranspose {d : ℕ} (A : BlockMat d) : BlockMat d

Public transpose operation for doubled block matrices.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.Book.Ch02.blockMatMul {d : ℕ} (A B : BlockMat d) : BlockMat d

Public multiplication operation for doubled block matrices.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.Book.Ch02.blockDiag {d : ℕ} (A B : Mat d) : BlockMat d

Public block diagonal matrix.

Equations

• HCPolySupport.Book.Ch02.blockDiag A B = { upperLeft := A, upperRight := 0, lowerLeft := 0, lowerRight := B }

def HCPolySupport.Book.Ch02.blockIdentity (d : ℕ) : BlockMat d

Public identity matrix in doubled block form.

Equations

• HCPolySupport.Book.Ch02.blockIdentity d = HCPolySupport.Book.Ch02.blockDiag 1 1

noncomputable def HCPolySupport.Book.Ch02.blockMatInv {d : ℕ} (A : BlockMat d) : BlockMat d

Public inverse operation for doubled block matrices, routed through the ordinary 2d × 2d matrix inverse.

Equations

• HCPolySupport.Book.Ch02.blockMatInv A = HCPolySupport.ofFullBlockMat (HCPolySupport.toFullBlockMat A)⁻¹

def HCPolySupport.Book.Ch02.blockG {d : ℕ} (h : Mat d) : BlockMat d

Public triangular block matrix G_h.

Equations

• HCPolySupport.Book.Ch02.blockG h = { upperLeft := 1, upperRight := 0, lowerLeft := h, lowerRight := 1 }

def HCPolySupport.Book.Ch02.blockR (d : ℕ) : BlockMat d

Public reflection block matrix R.

Equations

• HCPolySupport.Book.Ch02.blockR d = { upperLeft := 0, upperRight := 1, lowerLeft := 1, lowerRight := 0 }

def HCPolySupport.Book.Ch02.BlockPosDef {d : ℕ} (A : BlockMat d) : Prop

Positive definiteness for public doubled block matrices, expressed through the doubled quadratic form.

Equations

• HCPolySupport.Book.Ch02.BlockPosDef A = ∀ (X : HCPolySupport.BlockVec d), X ≠ 0 → 0 < HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul A X)

noncomputable def HCPolySupport.Book.Ch02.blockMatrixField {d : ℕ} {U : Domain d} (a : CoeffOn U) : Vec d → BlockMat d

The pointwise doubled coefficient matrix field \mathbf A(x) associated to the public coefficient representative. Public theorems about this field should use a.e. hypotheses/conclusions on U.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch02.blockMatrixInverseField {d : ℕ} {U : Domain d} (a : CoeffOn U) : Vec d → BlockMat d

The explicit inverse field appearing in e.block.matrix.inverse.basic.definitions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch02.blockEnergyDensityAt {d : ℕ} {U : Domain d} (a : CoeffOn U) (X : BlockVec d) (x : Vec d) : ℝ

Pointwise doubled energy density \frac12 X \cdot \mathbf A(x) X.

Equations

• HCPolySupport.Book.Ch02.blockEnergyDensityAt a X x = 1 / 2 * HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) X)

noncomputable def HCPolySupport.Book.Ch02.blockMatrixOfCoarseMatrices {d : ℕ} (M : CoarseMatrices d) : BlockMat d

The note-facing coarse block matrix assembled from the public coarse matrices sigma, sigmaStarInv, and kappa.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.isSymmetricBlockMat_blockMatrixOfCoarseMatrices {d : ℕ} (M : CoarseMatrices d) (hSigma : Matrix.IsSymm M.sigma) (hSigmaStarInv : Matrix.IsSymm M.sigmaStarInv) : IsSymmetricBlockMat (blockMatrixOfCoarseMatrices M)

The note-facing coarse block matrix assembled from the public coarse matrices is symmetric as a doubled block matrix.

noncomputable def HCPolySupport.Book.Ch02.coarseBlockMatrix {d : ℕ} (U : Domain d) (a : CoeffOn U) : BlockMat d

The canonical public coarse block matrix \mathbf A(U; a).

Equations

• HCPolySupport.Book.Ch02.coarseBlockMatrix U a = HCPolySupport.Book.Ch02.blockMatrixOfCoarseMatrices (HCPolySupport.Book.Ch02.coarseMatrices U a)

theorem HCPolySupport.Book.Ch02.isSymmetricBlockMat_coarseBlockMatrix {d : ℕ} (U : Domain d) (a : CoeffOn U) : IsSymmetricBlockMat (coarseBlockMatrix U a)

The canonical public coarse block matrix is symmetric as a doubled block matrix.

theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : coarseBlockMatrix U a = coarseBlockMatrix U b

noncomputable def HCPolySupport.Book.Ch02.coarseStarredBlockMatrixInv {d : ℕ} (U : Domain d) (a : CoeffOn U) : BlockMat d

The canonical public starred inverse block matrix \mathbf A_*^{-1}(U; a).

Equations

• HCPolySupport.Book.Ch02.coarseStarredBlockMatrixInv U a = HCPolySupport.blockReflect (HCPolySupport.Book.Ch02.coarseBlockMatrix U a)

noncomputable def HCPolySupport.Book.Ch02.coarseStarredBlockMatrix {d : ℕ} (U : Domain d) (a : CoeffOn U) : BlockMat d

The canonical public starred block matrix \mathbf A_*(U; a).

The notes introduce \mathbf A_* through the positive definite matrix whose inverse appears in the doubled response splitting.

Equations

• HCPolySupport.Book.Ch02.coarseStarredBlockMatrix U a = HCPolySupport.Book.Ch02.blockMatInv (HCPolySupport.Book.Ch02.coarseStarredBlockMatrixInv U a)

@[simp]

theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_upperLeft {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseBlockMatrix U a).upperLeft = bCoarse U a

@[simp]

theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_upperRight {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseBlockMatrix U a).upperRight = -(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a)

@[simp]

theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_lowerLeft {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseBlockMatrix U a).lowerLeft = -(sigmaStarInvCoarse U a * kappaCoarse U a)

@[simp]

theorem HCPolySupport.Book.Ch02.coarseBlockMatrix_lowerRight {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a

@[simp]

theorem HCPolySupport.Book.Ch02.coarseStarredBlockMatrixInv_eq_blockReflect {d : ℕ} (U : Domain d) (a : CoeffOn U) : coarseStarredBlockMatrixInv U a = blockReflect (coarseBlockMatrix U a)