Coarse-graining support: Support.CoarseGraining.Symmetric.CompletedSquare #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Completed squares for symmetric coefficient fields #
This file specializes the nonsymmetric magic identities to the symmetric case,
where kappa vanishes and the completed square is centered at
q = sigmaStar * p.
theorem
HCPolySupport.responseJ_completedSquare_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(ha : IsSymmetricCoeffField a)
(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)
:
theorem
HCPolySupport.responseJ_sigmaStar_mul_eq_half_gap_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(ha : IsSymmetricCoeffField a)
(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 : Vec d)
:
theorem
HCPolySupport.responseJ_sigmaStarCoarse_mul_eq_half_gap_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(ha : IsSymmetricCoeffField a)
(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 : Vec d)
:
ResponseJ U p (matVecMul (sigmaStarCoarse U a) p) a = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)