Coarse-graining support: Support.CoarseGraining.Symmetric.Response #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Symmetric response identities #
This file records the response-level consequences of the vanishing coupling matrix in the symmetric case.
theorem
HCPolySupport.kappa_eq_zero_of_isSymmetricCoeffField_of_isCoarseBlockMatrix_of_isKappaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{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)
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.responseJ_eq_add_p_zero_zero_q_sub_dot_of_isKappaCoarse_of_kappa_eq_zero
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hK : IsKappaCoarse U a sigmaStar kappa)
(hk : kappa = 0)
(p q : Vec d)
:
theorem
HCPolySupport.responseJ_eq_add_p_zero_zero_q_sub_dot_of_isSymmetricCoeffField
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{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)
(hdet : IsUnit (Matrix.det sigmaStar))
(p q : Vec d)
:
theorem
HCPolySupport.responseJ_p_zero_eq_half_vecDot_sigma_of_isSigmaCoarse_of_kappa_eq_zero
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hk : kappa = 0)
(p : Vec d)
:
theorem
HCPolySupport.responseJ_p_zero_eq_half_vecDot_sigma_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_p_zero_eq_half_vecDot_sigmaCoarse_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_zero_q_eq_half_vecDot_sigmaStar_inv_of_isSigmaStarCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(q : Vec d)
:
theorem
HCPolySupport.responseJ_zero_q_eq_half_vecDot_sigmaStarInvCoarse_of_isSigmaStarCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(q : Vec d)
:
theorem
HCPolySupport.responseJ_eq_half_vecDot_sigma_add_half_vecDot_sigmaStar_inv_sub_dot_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_eq_half_dot_sigmaCoarse_add_half_dot_sigmaStarInvCoarse_sub_dot
{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)
: