Coarse-graining support: #
Support.CoarseGraining.MagicIdentities.MuOrdering.EllipticConsequences.MagicIdentities
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
MuOrdering -- adjoint flipFlux magic identity wrappers #
Mu (p, -q) (adjointCoeffField a) - vecDot p q rewritten in
sigma, sigmaStar, kappa form, plus the shifted-square completion and the
canonical-coarse versions.
theorem
HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vecDot_of_isSigmaCoarse
{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)
:
theorem
HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vecDot_shifted_square_of_isSigmaCoarse
{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)
:
theorem
HCPolySupport.magic_identity_mu_adjointCoeffField_flipFlux_sub_vecDot_canonical_of_isSigmaCoarse
{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)
:
theorem
HCPolySupport.magicIdentity_mu_adjointFlux_sub_dot_eq_shiftedSquares
{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)
:
Mu U (p, -q) (adjointCoeffField a) - vecDot p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) - 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p)
(matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p))