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

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

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

Note-facing identities characterizing the coarse-grained matrices.

• sigma_symm : Matrix.IsSymm M.sigma
• sigmaStarInv_symm : Matrix.IsSymm M.sigmaStarInv
• sigmaStarInv_response (q : Vec d) : responseJ U a 0 q = 1 / 2 * vecDot q (matVecMul M.sigmaStarInv q)
• kappa_response (p q : Vec d) : mixedResponse U a p q = vecDot q (matVecMul M.sigmaStarInv (matVecMul M.kappa p))
• sigma_response (p : Vec d) : sigmaCorrectedResponse U a M p = 1 / 2 * vecDot p (matVecMul M.sigma p)
• full_response (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul M.sigma p) + 1 / 2 * vecDot (q + matVecMul M.kappa p) (matVecMul M.sigmaStarInv (q + matVecMul M.kappa p)) - vecDot p q

theorem HCPolySupport.Book.Ch02.ResponseMatrixIdentities.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {M : CoarseMatrices d} (hM : ResponseMatrixIdentities U a M) : ResponseMatrixIdentities U b M

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

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

The canonical note-facing matrix-extraction target: the matrices obtained directly from J satisfy the response identities.

Equations

• HCPolySupport.Book.Ch02.CanonicalResponseMatrixIdentities U a = HCPolySupport.Book.Ch02.ResponseMatrixIdentities U a (HCPolySupport.Book.Ch02.coarseMatrices U a)

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

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

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

Existence of public coarse-grained matrices satisfying the note-facing identities.

Equations

• HCPolySupport.Book.Ch02.ResponseMatrixExists U a = ∃ (M : HCPolySupport.Book.Ch02.CoarseMatrices d), HCPolySupport.Book.Ch02.ResponseMatrixIdentities U a M

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

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

theorem HCPolySupport.Book.Ch02.responseMatrixExists_of_canonicalResponseMatrixIdentities {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : CanonicalResponseMatrixIdentities U a) : ResponseMatrixExists U a

Canonical matrix identities imply the existential matrix-extraction statement.

noncomputable def HCPolySupport.Book.Ch02.responseMatrices {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) : CoarseMatrices d

Chosen public coarse-grained matrices, once the extraction theorem has been supplied.

Equations

• HCPolySupport.Book.Ch02.responseMatrices hM = Classical.choose hM

theorem HCPolySupport.Book.Ch02.responseMatrices_identities {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) : ResponseMatrixIdentities U a (responseMatrices hM)

noncomputable def HCPolySupport.Book.Ch02.sigmaMatrix {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) : Mat d

The σ matrix of a chosen coarse response representation supplied by matrix existence.

Equations

• HCPolySupport.Book.Ch02.sigmaMatrix hM = (HCPolySupport.Book.Ch02.responseMatrices hM).sigma

noncomputable def HCPolySupport.Book.Ch02.sigmaStarInvMatrix {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) : Mat d

The σ*⁻¹ matrix of a chosen coarse response representation supplied by matrix existence.

Equations

• HCPolySupport.Book.Ch02.sigmaStarInvMatrix hM = (HCPolySupport.Book.Ch02.responseMatrices hM).sigmaStarInv

noncomputable def HCPolySupport.Book.Ch02.kappaMatrix {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) : Mat d

The κ coupling matrix of a chosen coarse response representation supplied by matrix existence.

Equations

• HCPolySupport.Book.Ch02.kappaMatrix hM = (HCPolySupport.Book.Ch02.responseMatrices hM).kappa

theorem HCPolySupport.Book.Ch02.responseJ_eq_coarseMatrices_formula {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (hM : ResponseMatrixIdentities U a M) (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul M.sigma p) + 1 / 2 * vecDot (q + matVecMul M.kappa p) (matVecMul M.sigmaStarInv (q + matVecMul M.kappa p)) - vecDot p q

theorem HCPolySupport.Book.Ch02.responseJ_eq_canonical_coarseMatrices_formula {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : CanonicalResponseMatrixIdentities U a) (p q : Vec d) : responseJ U a 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

theorem HCPolySupport.Book.Ch02.responseJ_eq_responseMatrices_formula {d : ℕ} {U : Domain d} {a : CoeffOn U} (hM : ResponseMatrixExists U a) (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul (sigmaMatrix hM) p) + 1 / 2 * vecDot (q + matVecMul (kappaMatrix hM) p) (matVecMul (sigmaStarInvMatrix hM) (q + matVecMul (kappaMatrix hM) p)) - vecDot p q