Coarse-graining support: Support.Book.Ch02.Theorems.MagicIdentitiesDefinitions

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

structure HCPolySupport.Book.Ch02.ResponseMagicIdentitiesTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for l.magic.identities.basic.definitions.

The canonical public theorem proving this package is responseMagicIdentitiesTheory in MagicIdentities.lean.

• completed_square (p q : Vec d) : responseJ U a 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))
• adjoint_quadratic (p q : Vec d) : responseJ U a.transpose p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (kappaCoarse U a) p)) - vecDot p q
• response_adjoint_sum (p q h : Vec d) : responseJ U a p (q - h) + responseJ U a.transpose p (q + h) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p)) + vecDot (h - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (h - matVecMul (kappaCoarse U a) p))
• diagonal_magic (e : Vec d) : responseJ U a e (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) e) + responseJ U a.transpose e (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) e) = vecDot e (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) e)
• sigmaStar_le_sigma : MatLoewnerLE (sigmaStarCoarse U a) (sigmaCoarse U a)
• kappa_symm_le_defect : MatLoewnerLE (kappaCoarse U a + matTranspose (kappaCoarse U a)) (sigmaCoarse U a - sigmaStarCoarse U a)
• neg_kappa_symm_le_defect : MatLoewnerLE (-(kappaCoarse U a + matTranspose (kappaCoarse U a))) (sigmaCoarse U a - sigmaStarCoarse U a)

theorem HCPolySupport.Book.Ch02.ResponseMagicIdentitiesTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (hTheory : ResponseMagicIdentitiesTheory U a) : ResponseMagicIdentitiesTheory U b

The magic identities depend only on the public coefficient representative up to a.e. equality on the domain.

theorem HCPolySupport.Book.Ch02.ResponseMagicIdentitiesTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : ResponseMagicIdentitiesTheory U a ↔ ResponseMagicIdentitiesTheory U b

A.e.-equivalent coefficient representatives satisfy the same magic identity package.