Coarse-graining support: Support.CoarseGraining.BlockMatrixProperties

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

Phase-1 structural bookkeeping for the canonical coarse block matrices.

This file implements the first deterministic slice from internal planning notes. It focuses on the algebraic bookkeeping around the Chapter-2 note label l.block.coarse.matrices.basic.definitions:

• expose the blocks of coarseBlockMatrix U a;
• record the reflection identity defining coarseStarredBlockMatrixInv U a;
• package the canonical deterministic block candidates built from sigmaStarInvCoarse, sigmaStarInvKappaCoarse, kappaCoarse, and sigmaCoarse;
• relate those canonical candidates to arbitrary deterministic witness data once the defining hypotheses are available.

This file deliberately avoids the heavier variational proofs reserved for later deterministic modules.

theorem HCPolySupport.coarseBlockMatrix_upperLeft_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : (coarseBlockMatrix U a).upperLeft i j = if i = j then 2 * Mu U (Pi.single i 1, 0) a else Mu U ((Pi.single i 1, 0) + (Pi.single j 1, 0)) a - Mu U (Pi.single i 1, 0) a - Mu U (Pi.single j 1, 0) a

Phase-1 bookkeeping for the upper-left block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_upperRight_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : (coarseBlockMatrix U a).upperRight i j = Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a - Mu U (Pi.single i 1, 0) a - Mu U (0, Pi.single j 1) a

Phase-1 bookkeeping for the upper-right block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : (coarseBlockMatrix U a).lowerLeft i j = Mu U ((0, Pi.single i 1) + (Pi.single j 1, 0)) a - Mu U (0, Pi.single i 1) a - Mu U (Pi.single j 1, 0) a

Phase-1 bookkeeping for the lower-left block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerRight_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i j : Fin d) : (coarseBlockMatrix U a).lowerRight i j = if i = j then 2 * Mu U (0, Pi.single i 1) a else Mu U ((0, Pi.single i 1) + (0, Pi.single j 1)) a - Mu U (0, Pi.single i 1) a - Mu U (0, Pi.single j 1) a

Phase-1 bookkeeping for the lower-right block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_upperLeft_apply_diag {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i : Fin d) : (coarseBlockMatrix U a).upperLeft i i = 2 * Mu U (Pi.single i 1, 0) a

Phase-1 bookkeeping for the diagonal entries of the upper-left block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_upperLeft_apply_offDiag {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {i j : Fin d} (hij : i ≠ j) : (coarseBlockMatrix U a).upperLeft i j = Mu U ((Pi.single i 1, 0) + (Pi.single j 1, 0)) a - Mu U (Pi.single i 1, 0) a - Mu U (Pi.single j 1, 0) a

Phase-1 bookkeeping for the off-diagonal entries of the upper-left block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerRight_apply_diag {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (i : Fin d) : (coarseBlockMatrix U a).lowerRight i i = 2 * Mu U (0, Pi.single i 1) a

Phase-1 bookkeeping for the diagonal entries of the lower-right block of the canonical coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerRight_apply_offDiag {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {i j : Fin d} (hij : i ≠ j) : (coarseBlockMatrix U a).lowerRight i j = Mu U ((0, Pi.single i 1) + (0, Pi.single j 1)) a - Mu U (0, Pi.single i 1) a - Mu U (0, Pi.single j 1) a

Phase-1 bookkeeping for the off-diagonal entries of the lower-right block of the canonical coarse matrix \mathbf A(U; a).

@[simp]

theorem HCPolySupport.coarseStarredBlockMatrixInv_eq_blockReflect {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : coarseStarredBlockMatrixInv U a = blockReflect (coarseBlockMatrix U a)

Deterministic bookkeeping lemmas for the canonical coarse matrices.

This theorem layer packages the note-facing block matrices built from the current canonical deterministic quantities and records the equalities they satisfy once the relevant witness hypotheses are available.

noncomputable def HCPolySupport.blockMatrixOfDeterministicData {d : ℕ} (sigma sigmaStar kappa : Mat d) : BlockMat d

The note-faithful coarse block matrix attached to deterministic data (sigma, sigmaStar, kappa).

Equations

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

@[simp]

theorem HCPolySupport.blockMatrixOfDeterministicData_upperLeft {d : ℕ} (sigma sigmaStar kappa : Mat d) : (blockMatrixOfDeterministicData sigma sigmaStar kappa).upperLeft = bCoarse sigma sigmaStar kappa

@[simp]

theorem HCPolySupport.blockMatrixOfDeterministicData_upperRight {d : ℕ} (sigma sigmaStar kappa : Mat d) : (blockMatrixOfDeterministicData sigma sigmaStar kappa).upperRight = -(matTranspose kappa * sigmaStar⁻¹)

@[simp]

theorem HCPolySupport.blockMatrixOfDeterministicData_lowerLeft {d : ℕ} (sigma sigmaStar kappa : Mat d) : (blockMatrixOfDeterministicData sigma sigmaStar kappa).lowerLeft = -(sigmaStar⁻¹ * kappa)

@[simp]

theorem HCPolySupport.blockMatrixOfDeterministicData_lowerRight {d : ℕ} (sigma sigmaStar kappa : Mat d) : (blockMatrixOfDeterministicData sigma sigmaStar kappa).lowerRight = sigmaStar⁻¹

theorem HCPolySupport.blockMatrixOfDeterministicData_upperLeft_smul {d : ℕ} {sigma sigmaStar kappa : Mat d} (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) : (blockMatrixOfDeterministicData (lam • sigma) (lam • sigmaStar) (lam • kappa)).upperLeft = lam • (blockMatrixOfDeterministicData sigma sigmaStar kappa).upperLeft

theorem HCPolySupport.blockMatrixOfDeterministicData_upperRight_smul {d : ℕ} {sigma sigmaStar kappa : Mat d} (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) : (blockMatrixOfDeterministicData (lam • sigma) (lam • sigmaStar) (lam • kappa)).upperRight = (blockMatrixOfDeterministicData sigma sigmaStar kappa).upperRight

theorem HCPolySupport.blockMatrixOfDeterministicData_lowerLeft_smul {d : ℕ} {sigma sigmaStar kappa : Mat d} (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) : (blockMatrixOfDeterministicData (lam • sigma) (lam • sigmaStar) (lam • kappa)).lowerLeft = (blockMatrixOfDeterministicData sigma sigmaStar kappa).lowerLeft

theorem HCPolySupport.blockMatrixOfDeterministicData_lowerRight_smul {d : ℕ} {sigma sigmaStar kappa : Mat d} (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) : (blockMatrixOfDeterministicData (lam • sigma) (lam • sigmaStar) (lam • kappa)).lowerRight = lam⁻¹ • (blockMatrixOfDeterministicData sigma sigmaStar kappa).lowerRight

noncomputable def HCPolySupport.starredBlockMatrixInvOfDeterministicData {d : ℕ} (sigma sigmaStar kappa : Mat d) : BlockMat d

The reflected note-faithful starred inverse block matrix attached to deterministic data (sigma, sigmaStar, kappa).

Equations

• HCPolySupport.starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa = HCPolySupport.blockReflect (HCPolySupport.blockMatrixOfDeterministicData sigma sigmaStar kappa)

@[simp]

theorem HCPolySupport.starredBlockMatrixInvOfDeterministicData_eq_blockReflect {d : ℕ} (sigma sigmaStar kappa : Mat d) : starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa = blockReflect (blockMatrixOfDeterministicData sigma sigmaStar kappa)

@[simp]

theorem HCPolySupport.starredBlockMatrixInvOfDeterministicData_upperLeft {d : ℕ} (sigma sigmaStar kappa : Mat d) : (starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa).upperLeft = sigmaStar⁻¹

@[simp]

theorem HCPolySupport.starredBlockMatrixInvOfDeterministicData_upperRight {d : ℕ} (sigma sigmaStar kappa : Mat d) : (starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa).upperRight = -(sigmaStar⁻¹ * kappa)

@[simp]

theorem HCPolySupport.starredBlockMatrixInvOfDeterministicData_lowerLeft {d : ℕ} (sigma sigmaStar kappa : Mat d) : (starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa).lowerLeft = -(matTranspose kappa * sigmaStar⁻¹)

@[simp]

theorem HCPolySupport.starredBlockMatrixInvOfDeterministicData_lowerRight {d : ℕ} (sigma sigmaStar kappa : Mat d) : (starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa).lowerRight = bCoarse sigma sigmaStar kappa

noncomputable def HCPolySupport.deterministicCoarseBlockMatrix {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : BlockMat d

The coarse block candidate built from the canonical deterministic coarse pieces already defined in Definitions.lean.

Equations

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

@[simp]

theorem HCPolySupport.deterministicCoarseBlockMatrix_upperLeft {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicCoarseBlockMatrix U a).upperLeft = sigmaCoarse U a + matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a * kappaCoarse U a

@[simp]

theorem HCPolySupport.deterministicCoarseBlockMatrix_upperRight {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicCoarseBlockMatrix U a).upperRight = -(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a)

@[simp]

theorem HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicCoarseBlockMatrix U a).lowerLeft = -sigmaStarInvKappaCoarse U a

@[simp]

theorem HCPolySupport.deterministicCoarseBlockMatrix_lowerRight {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicCoarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a

noncomputable def HCPolySupport.deterministicStarredBlockMatrixInv {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : BlockMat d

The reflected starred inverse block candidate built from the canonical deterministic coarse pieces.

Equations

• HCPolySupport.deterministicStarredBlockMatrixInv U a = HCPolySupport.blockReflect (HCPolySupport.deterministicCoarseBlockMatrix U a)

@[simp]

theorem HCPolySupport.deterministicStarredBlockMatrixInv_eq_blockReflect {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : deterministicStarredBlockMatrixInv U a = blockReflect (deterministicCoarseBlockMatrix U a)

@[simp]

theorem HCPolySupport.deterministicStarredBlockMatrixInv_upperLeft {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicStarredBlockMatrixInv U a).upperLeft = sigmaStarInvCoarse U a

@[simp]

theorem HCPolySupport.deterministicStarredBlockMatrixInv_upperRight {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicStarredBlockMatrixInv U a).upperRight = -sigmaStarInvKappaCoarse U a

@[simp]

theorem HCPolySupport.deterministicStarredBlockMatrixInv_lowerLeft {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicStarredBlockMatrixInv U a).lowerLeft = -(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a)

@[simp]

theorem HCPolySupport.deterministicStarredBlockMatrixInv_lowerRight {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : (deterministicStarredBlockMatrixInv U a).lowerRight = sigmaCoarse U a + matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a * kappaCoarse U a

theorem HCPolySupport.deterministicCoarseBlockMatrix_eq_blockMatrixOfDeterministicData_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : deterministicCoarseBlockMatrix U a = blockMatrixOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.deterministicCoarseBlockMatrix_eq_blockMatrixOfDeterministicData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : deterministicCoarseBlockMatrix U a = blockMatrixOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.deterministicStarredBlockMatrixInv_eq_starredBlockMatrixInvOfDeterministicData_of_isSigmaCoarse {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : deterministicStarredBlockMatrixInv U a = starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.deterministicStarredBlockMatrixInv_eq_starredBlockMatrixInvOfDeterministicData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : deterministicStarredBlockMatrixInv U a = starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.coarseBlockMatrix_eq_deterministicCoarseBlockMatrix_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : coarseBlockMatrix U a = deterministicCoarseBlockMatrix U a

theorem HCPolySupport.coarseBlockMatrix_eq_deterministicCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : coarseBlockMatrix U a = deterministicCoarseBlockMatrix U a

theorem HCPolySupport.coarseBlockMatrix_eq_blockMatrixOfDeterministicData_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : coarseBlockMatrix U a = blockMatrixOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.coarseBlockMatrix_upperLeft_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseBlockMatrix U a).upperLeft = sigmaCoarse U a + matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a * kappaCoarse U a

Canonical upper-left block formula for \mathbf A(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseBlockMatrix_upperRight_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseBlockMatrix U a).upperRight = -(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a)

Canonical upper-right block formula for \mathbf A(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseBlockMatrix U a).lowerLeft = -sigmaStarInvKappaCoarse U a

Canonical lower-left block formula for \mathbf A(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseBlockMatrix_lowerRight_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a

Canonical lower-right block formula for \mathbf A(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseBlockMatrix_upperLeft_eq_bCoarse_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseBlockMatrix U a).upperLeft = bCoarse sigma sigmaStar kappa

Public upper-left block formula for the coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_upperRight_eq_neg_transpose_kappa_mul_sigmaStar_inv_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseBlockMatrix U a).upperRight = -(matTranspose kappa * sigmaStar⁻¹)

Public upper-right block formula for the coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerLeft_eq_neg_sigmaStar_inv_mul_kappa_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseBlockMatrix U a).lowerLeft = -(sigmaStar⁻¹ * kappa)

Public lower-left block formula for the coarse matrix \mathbf A(U; a).

theorem HCPolySupport.coarseBlockMatrix_lowerRight_eq_sigmaStar_inv_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseBlockMatrix U a).lowerRight = sigmaStar⁻¹

Public lower-right block formula for the coarse matrix \mathbf A(U; a).

theorem HCPolySupport.blockMatVecMul_coarseBlockMatrix_fst_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : (blockMatVecMul (coarseBlockMatrix U a) (p, q)).1 = matVecMul sigma p - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p))

Public formula for the first component of \mathbf A(U; a) (p, q).

theorem HCPolySupport.blockMatVecMul_coarseBlockMatrix_snd_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : (blockMatVecMul (coarseBlockMatrix U a) (p, q)).2 = matVecMul sigmaStar⁻¹ (q - matVecMul kappa p)

Public formula for the second component of \mathbf A(U; a) (p, q).

theorem HCPolySupport.blockMatVecMul_coarseBlockMatrix_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : blockMatVecMul (coarseBlockMatrix U a) (p, q) = (matVecMul sigma p - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p)), matVecMul sigmaStar⁻¹ (q - matVecMul kappa p))

Public formula for \mathbf A(U; a) (p, q).

theorem HCPolySupport.coarseStarredBlockMatrixInv_eq_deterministicStarredBlockMatrixInv_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : coarseStarredBlockMatrixInv U a = deterministicStarredBlockMatrixInv U a

theorem HCPolySupport.coarseStarredBlockMatrixInv_eq_deterministicStarredBlockMatrixInv {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : coarseStarredBlockMatrixInv U a = deterministicStarredBlockMatrixInv U a

theorem HCPolySupport.coarseStarredMatrixInv_eq_deterministic_of_coarseData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : coarseStarredBlockMatrixInv U a = starredBlockMatrixInvOfDeterministicData sigma sigmaStar kappa

theorem HCPolySupport.isSigmaStarInvCoarse_coarseBlockMatrix_lowerRight_of_mu_zero_right_eq_responseJ_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) : IsSigmaStarInvCoarse U a (coarseBlockMatrix U a).lowerRight

If the pure-flux slice of \mu matches the pure-flux slice of \mathcal J, then the lower-right block of the canonical coarse block matrix realizes the canonical \sigma_*^{-1}(U; a) data.

theorem HCPolySupport.coarseBlockMatrix_lowerRight_eq_sigmaStarInvCoarse_of_mu_zero_right_eq_responseJ_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) : (coarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a

If the pure-flux slice of \mu matches the pure-flux slice of \mathcal J, then the lower-right block of the canonical coarse block matrix is the canonical \sigma_*^{-1}(U; a).

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_eq_sigmaStarInvCoarse_of_mu_zero_right_eq_responseJ_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hex : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar) (hMuResp : ∀ (q : Vec d), Mu U (0, q) a = ResponseJ U 0 q a) : (coarseStarredBlockMatrixInv U a).upperLeft = sigmaStarInvCoarse U a

If the pure-flux slice of \mu matches the pure-flux slice of \mathcal J, then the upper-left block of \mathbf A_*^{-1}(U; a) is the canonical \sigma_*^{-1}(U; a).

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseStarredBlockMatrixInv U a).upperLeft = sigmaStarInvCoarse U a

Canonical upper-left block formula for \mathbf A_*^{-1}(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperRight_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseStarredBlockMatrixInv U a).upperRight = -sigmaStarInvKappaCoarse U a

Canonical upper-right block formula for \mathbf A_*^{-1}(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerLeft_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseStarredBlockMatrixInv U a).lowerLeft = -(matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a)

Canonical lower-left block formula for \mathbf A_*^{-1}(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_eq_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) : (coarseStarredBlockMatrixInv U a).lowerRight = sigmaCoarse U a + matTranspose (kappaCoarse U a) * sigmaStarInvCoarse U a * kappaCoarse U a

Canonical lower-right block formula for \mathbf A_*^{-1}(U; a) once the deterministic coarse candidate is identified as coarse.

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_eq_sigmaStar_inv_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseStarredBlockMatrixInv U a).upperLeft = sigmaStar⁻¹

Public upper-left block formula for the reflected coarse matrix \mathbf A_*^{-1}(U; a).

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperRight_eq_neg_sigmaStar_inv_mul_kappa_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseStarredBlockMatrixInv U a).upperRight = -(sigmaStar⁻¹ * kappa)

Public upper-right block formula for the reflected coarse matrix \mathbf A_*^{-1}(U; a).

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerLeft_eq_neg_transpose_kappa_mul_sigmaStar_inv {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseStarredBlockMatrixInv U a).lowerLeft = -(matTranspose kappa * sigmaStar⁻¹)

Public lower-left block formula for the reflected coarse matrix \mathbf A_*^{-1}(U; a).

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_eq_bCoarse_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) : (coarseStarredBlockMatrixInv U a).lowerRight = bCoarse sigma sigmaStar kappa

Public lower-right block formula for the reflected coarse matrix \mathbf A_*^{-1}(U; a).

theorem HCPolySupport.blockMatVecMul_coarseStarredBlockMatrixInv_fst_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : (blockMatVecMul (coarseStarredBlockMatrixInv U a) (p, q)).1 = matVecMul sigmaStar⁻¹ (p - matVecMul kappa q)

Public formula for the first component of \mathbf A_*^{-1}(U; a) (p, q).

theorem HCPolySupport.blockMatVecMul_coarseStarredBlockMatrixInv_snd_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : (blockMatVecMul (coarseStarredBlockMatrixInv U a) (p, q)).2 = matVecMul sigma q - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ (p - matVecMul kappa q))

Public formula for the second component of \mathbf A_*^{-1}(U; a) (p, q).

theorem HCPolySupport.blockMatVecMul_coarseStarredBlockMatrixInv_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : blockMatVecMul (coarseStarredBlockMatrixInv U a) (p, q) = (matVecMul sigmaStar⁻¹ (p - matVecMul kappa q), matVecMul sigma q - matVecMul (matTranspose kappa) (matVecMul sigmaStar⁻¹ (p - matVecMul kappa q)))

Public formula for \mathbf A_*^{-1}(U; a) (p, q).