Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.Symmetric.CoarseMatrices

Coarse-graining support: Support.CoarseGraining.Symmetric.CoarseMatrices #

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

Symmetric coefficient fields and coarse matrices #

This file specializes the deterministic coarse-matrix API to pointwise symmetric coefficient fields. The main structural consequence is that the canonical coupling matrix kappaCoarse vanishes.

source
@[simp]
theorem HCPolySupport.bCoarse_zero_right {d : ℕ} (sigma sigmaStar : Mat d) :
bCoarse sigma sigmaStar 0 = sigma
source
@[simp]
theorem HCPolySupport.aCoarse_zero_right {d : ℕ} (sigma : Mat d) :
aCoarse sigma 0 = sigma
source
@[simp]
theorem HCPolySupport.aStarCoarse_zero_right {d : ℕ} (sigmaStar : Mat d) :
aStarCoarse sigmaStar 0 = sigmaStar
source
theorem HCPolySupport.sigmaStarInvKappaCoarse_eq_zero_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
sigmaStarInvKappaCoarse U a = 0
source
theorem HCPolySupport.kappaCoarse_eq_zero_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
kappaCoarse U a = 0
source
theorem HCPolySupport.coarseBlockMatrix_lowerLeft_eq_zero_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
(coarseBlockMatrix U a).lowerLeft = 0
source
theorem HCPolySupport.coarseBlockMatrix_upperRight_eq_zero_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
(coarseBlockMatrix U a).upperRight = 0
source
theorem HCPolySupport.coarseBlockMatrix_upperLeft_eq_sigmaCoarse_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
(coarseBlockMatrix U a).upperLeft = sigmaCoarse U a
source
theorem HCPolySupport.coarseBlockMatrix_lowerRight_eq_sigmaStarInvCoarse_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (_ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
(coarseBlockMatrix U a).lowerRight = sigmaStarInvCoarse U a
source
theorem HCPolySupport.bCoarse_canonical_eq_sigmaCoarse_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
bCoarse (sigmaCoarse U a) (sigmaStarCoarse U a) (kappaCoarse U a) = sigmaCoarse U a
source
theorem HCPolySupport.aCoarse_canonical_eq_sigmaCoarse_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
aCoarse (sigmaCoarse U a) (kappaCoarse U a) = sigmaCoarse U a
source
theorem HCPolySupport.aStarCoarse_canonical_eq_sigmaStarCoarse_of_isSymmetricCoeffField_of_isCoarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a)) :
aStarCoarse (sigmaStarCoarse U a) (kappaCoarse U a) = sigmaStarCoarse U a