Coarse-graining support: Support.Book.Ch02.Matrices

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

noncomputable def HCPolySupport.Book.Ch02.averageMat {d : ℕ} (U : Domain d) (A : Vec d → Mat d) : Mat d

Public normalized matrix average over a Chapter 2 domain.

Equations

• HCPolySupport.Book.Ch02.averageMat U A i j = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => A x i j

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

The note-facing harmonic-mean matrix \fint_U symmPart(a)^{-1}.

Equations

• HCPolySupport.Book.Ch02.averagedSymmPartInv U a = HCPolySupport.Book.Ch02.averageMat U fun (x : HCPolySupport.Vec d) => (HCPolySupport.symmPart (a.toCoeffField x))⁻¹

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

The note-facing upper coefficient average \fint_U (symmPart(a) + skewPart(a)^t symmPart(a)^{-1} skewPart(a)).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.averagedSymmPartInv_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : averagedSymmPartInv U a = averagedSymmPartInv U b

The harmonic-mean matrix depends only on the coefficient field up to a.e. equality on the domain.

theorem HCPolySupport.Book.Ch02.averagedSymmPartPlusCorrection_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : averagedSymmPartPlusCorrection U a = averagedSymmPartPlusCorrection U b

The upper coefficient average depends only on the coefficient field up to a.e. equality on the domain.

structure HCPolySupport.Book.Ch02.CoarseMatrices (d : ℕ) : Type

The coarse-grained response matrices extracted from the quadratic response functional. We keep sigmaStarInv primitive at this stage; constructing sigmaStar itself belongs to the later positivity/invertibility theorem.

• sigma : Mat d

  The matrix parameter σ in the coarse quadratic response representation.

• sigmaStarInv : Mat d

  The primitive matrix parameter representing σ*⁻¹ in the coarse quadratic response.

• kappa : Mat d

  The coupling matrix κ in the coarse quadratic response representation.

noncomputable def HCPolySupport.Book.Ch02.CoarseMatrices.sigmaStar {d : ℕ} (M : CoarseMatrices d) : Mat d

The derived coarse matrix sigmaStar = sigmaStarInv^{-1}.

Equations

• M.sigmaStar = M.sigmaStarInv⁻¹

def HCPolySupport.Book.Ch02.CoarseMatrices.b {d : ℕ} (M : CoarseMatrices d) : Mat d

The derived coarse matrix b = sigma + kappa^t sigmaStarInv kappa.

Equations

• M.b = M.sigma + HCPolySupport.matTranspose M.kappa * M.sigmaStarInv * M.kappa

def HCPolySupport.Book.Ch02.CoarseMatrices.coeff {d : ℕ} (M : CoarseMatrices d) : Mat d

The derived coarse coefficient matrix a = sigma - kappa^t.

Equations

• M.coeff = M.sigma - HCPolySupport.matTranspose M.kappa

theorem HCPolySupport.Book.Ch02.CoarseMatrices.ext {d : ℕ} {M N : CoarseMatrices d} (hsigma : M.sigma = N.sigma) (hsigmaStarInv : M.sigmaStarInv = N.sigmaStarInv) (hkappa : M.kappa = N.kappa) : M = N

theorem HCPolySupport.Book.Ch02.CoarseMatrices.ext_iff {d : ℕ} {M N : CoarseMatrices d} : M = N ↔ M.sigma = N.sigma ∧ M.sigmaStarInv = N.sigmaStarInv ∧ M.kappa = N.kappa

noncomputable def HCPolySupport.Book.Ch02.mixedResponse {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : ℝ

The mixed response appearing in the definition of the coarse skew matrix.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch02.sigmaStarInvEntry {d : ℕ} (U : Domain d) (a : CoeffOn U) (i j : Fin d) : ℝ

Entry formula for the canonical coarse matrix sigmaStarInv.

The diagonal entries are extracted from the pure q response, while the off-diagonal entries use the usual polarization identity.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.sigmaStarInvEntry_comm {d : ℕ} (U : Domain d) (a : CoeffOn U) (i j : Fin d) : sigmaStarInvEntry U a i j = sigmaStarInvEntry U a j i

The entry formula for sigmaStarInv is symmetric by construction.

theorem HCPolySupport.Book.Ch02.sigmaStarInvEntry_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (i j : Fin d) : sigmaStarInvEntry U a i j = sigmaStarInvEntry U b i j

The entry formula for sigmaStarInv depends only on the coefficient field up to a.e. equality on the domain.

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

The canonical coarse matrix sigmaStarInv(U; a) extracted from J(U,0,q;a).

Equations

• HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a i j = HCPolySupport.Book.Ch02.sigmaStarInvEntry U a i j

theorem HCPolySupport.Book.Ch02.sigmaStarInvCoarse_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (sigmaStarInvCoarse U a)

The canonical matrix sigmaStarInv(U; a) is symmetric by polarization.

theorem HCPolySupport.Book.Ch02.sigmaStarInvCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : sigmaStarInvCoarse U a = sigmaStarInvCoarse U b

The canonical matrix sigmaStarInv(U; a) is invariant under a.e. changes of coefficient representative.

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

The canonical coarse matrix sigmaStar(U; a), represented as the nonsingular-inverse expression of sigmaStarInv(U; a). The later positivity theory proves that this is the genuine inverse in the note-facing cases.

Equations

• HCPolySupport.Book.Ch02.sigmaStarCoarse U a = (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a)⁻¹

theorem HCPolySupport.Book.Ch02.sigmaStarCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : sigmaStarCoarse U a = sigmaStarCoarse U b

The canonical matrix sigmaStar(U; a) is invariant under a.e. changes of coefficient representative.

theorem HCPolySupport.Book.Ch02.sigmaStarCoarse_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (sigmaStarCoarse U a)

The canonical matrix sigmaStar(U; a) is symmetric.

theorem HCPolySupport.Book.Ch02.mixedResponse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) : mixedResponse U a p q = mixedResponse U b p q

The mixed response depends only on the coefficient field up to a.e. equality on the domain.

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

The canonical mixed matrix sigmaStarInv(U; a) * kappa(U; a), extracted directly from the mixed response.

Equations

• HCPolySupport.Book.Ch02.sigmaStarInvKappaCoarse U a i j = HCPolySupport.Book.Ch02.mixedResponse U a (Pi.single j 1) (Pi.single i 1)

theorem HCPolySupport.Book.Ch02.sigmaStarInvKappaCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : sigmaStarInvKappaCoarse U a = sigmaStarInvKappaCoarse U b

The canonical mixed matrix is invariant under a.e. changes of coefficient representative.

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

The canonical coupling matrix kappa(U; a).

Equations

• HCPolySupport.Book.Ch02.kappaCoarse U a = HCPolySupport.Book.Ch02.sigmaStarCoarse U a * HCPolySupport.Book.Ch02.sigmaStarInvKappaCoarse U a

theorem HCPolySupport.Book.Ch02.kappaCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : kappaCoarse U a = kappaCoarse U b

The canonical coupling matrix is invariant under a.e. changes of coefficient representative.

theorem HCPolySupport.Book.Ch02.sigmaStarInvCoarse_mul_sigmaStarCoarse {d : ℕ} {U : Domain d} {a : CoeffOn U} (hdet : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) : sigmaStarInvCoarse U a * sigmaStarCoarse U a = 1

Under nondegeneracy, sigmaStar(U; a) is the right inverse of sigmaStarInv(U; a).

theorem HCPolySupport.Book.Ch02.sigmaStarCoarse_mul_sigmaStarInvCoarse {d : ℕ} {U : Domain d} {a : CoeffOn U} (hdet : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) : sigmaStarCoarse U a * sigmaStarInvCoarse U a = 1

Under nondegeneracy, sigmaStar(U; a) is the left inverse of sigmaStarInv(U; a).

theorem HCPolySupport.Book.Ch02.sigmaStarInvCoarse_mul_kappaCoarse_eq_sigmaStarInvKappaCoarse {d : ℕ} {U : Domain d} {a : CoeffOn U} (hdet : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) : sigmaStarInvCoarse U a * kappaCoarse U a = sigmaStarInvKappaCoarse U a

Under nondegeneracy, the canonical kappa definition really solves sigmaStarInv * kappa = sigmaStarInvKappa.

theorem HCPolySupport.Book.Ch02.matVecMul_sigmaStarInvCoarse_kappaCoarse {d : ℕ} {U : Domain d} {a : CoeffOn U} (hdet : IsUnit (Matrix.det (sigmaStarInvCoarse U a))) (p : Vec d) : matVecMul (sigmaStarInvCoarse U a) (matVecMul (kappaCoarse U a) p) = matVecMul (sigmaStarInvKappaCoarse U a) p

Vector form of sigmaStarInvCoarse_mul_kappaCoarse_eq_sigmaStarInvKappaCoarse.

noncomputable def HCPolySupport.Book.Ch02.canonicalSigmaCorrectedResponse {d : ℕ} (U : Domain d) (a : CoeffOn U) (p : Vec d) : ℝ

The canonical corrected p-response whose quadratic form defines sigma(U; a).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.canonicalSigmaCorrectedResponse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p : Vec d) : canonicalSigmaCorrectedResponse U a p = canonicalSigmaCorrectedResponse U b p

The canonical corrected response is invariant under a.e. changes of coefficient representative.

noncomputable def HCPolySupport.Book.Ch02.sigmaEntry {d : ℕ} (U : Domain d) (a : CoeffOn U) (i j : Fin d) : ℝ

Entry formula for the canonical coarse matrix sigma.

As for sigmaStarInv, the diagonal entries come from the quadratic values and the off-diagonal entries from polarization.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.sigmaEntry_comm {d : ℕ} (U : Domain d) (a : CoeffOn U) (i j : Fin d) : sigmaEntry U a i j = sigmaEntry U a j i

The entry formula for sigma is symmetric by construction.

theorem HCPolySupport.Book.Ch02.sigmaEntry_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (i j : Fin d) : sigmaEntry U a i j = sigmaEntry U b i j

The entry formula for sigma depends only on the coefficient field up to a.e. equality on the domain.

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

The canonical coarse matrix sigma(U; a).

Equations

• HCPolySupport.Book.Ch02.sigmaCoarse U a i j = HCPolySupport.Book.Ch02.sigmaEntry U a i j

theorem HCPolySupport.Book.Ch02.sigmaCoarse_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (sigmaCoarse U a)

The canonical matrix sigma(U; a) is symmetric by polarization.

theorem HCPolySupport.Book.Ch02.sigmaCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : sigmaCoarse U a = sigmaCoarse U b

The canonical matrix sigma(U; a) is invariant under a.e. changes of coefficient representative.

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

The canonical package of coarse-grained response matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.coarseMatrices_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : coarseMatrices U a = coarseMatrices U b

The canonical package of coarse-grained response matrices is invariant under a.e. changes of coefficient representative.

theorem HCPolySupport.Book.Ch02.coarseMatrices_sigma_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (coarseMatrices U a).sigma

The sigma component of the canonical matrix package is symmetric.

theorem HCPolySupport.Book.Ch02.coarseMatrices_sigmaStarInv_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (coarseMatrices U a).sigmaStarInv

The sigmaStarInv component of the canonical matrix package is symmetric.

noncomputable def HCPolySupport.Book.Ch02.sigmaCorrectedResponse {d : ℕ} (U : Domain d) (a : CoeffOn U) (M : CoarseMatrices d) (p : Vec d) : ℝ

The corrected p-response whose quadratic form defines sigma.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.sigmaCorrectedResponse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (M : CoarseMatrices d) (p : Vec d) : sigmaCorrectedResponse U a M p = sigmaCorrectedResponse U b M p

The corrected response for a fixed matrix package depends only on the coefficient field up to a.e. equality on the domain.

@[simp]

theorem HCPolySupport.Book.Ch02.coarseMatrices_sigma {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseMatrices U a).sigma = sigmaCoarse U a

@[simp]

theorem HCPolySupport.Book.Ch02.coarseMatrices_sigmaStarInv {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseMatrices U a).sigmaStarInv = sigmaStarInvCoarse U a

@[simp]

theorem HCPolySupport.Book.Ch02.coarseMatrices_sigmaStar {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseMatrices U a).sigmaStar = sigmaStarCoarse U a

@[simp]

theorem HCPolySupport.Book.Ch02.coarseMatrices_kappa {d : ℕ} (U : Domain d) (a : CoeffOn U) : (coarseMatrices U a).kappa = kappaCoarse U a

theorem HCPolySupport.Book.Ch02.sigmaCorrectedResponse_coarseMatrices {d : ℕ} (U : Domain d) (a : CoeffOn U) (p : Vec d) : sigmaCorrectedResponse U a (coarseMatrices U a) p = canonicalSigmaCorrectedResponse U a p

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

Canonical derived coarse matrix b(U; a) = sigma + kappa^t sigmaStarInv kappa.

Equations

• HCPolySupport.Book.Ch02.bCoarse U a = (HCPolySupport.Book.Ch02.coarseMatrices U a).b

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

Canonical derived coarse coefficient matrix a(U; a) = sigma - kappa^t.

Equations

• HCPolySupport.Book.Ch02.aCoarse U a = (HCPolySupport.Book.Ch02.coarseMatrices U a).coeff

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

Canonical derived adjoint coarse coefficient matrix.

Equations

• HCPolySupport.Book.Ch02.aStarCoarse U a = HCPolySupport.Book.Ch02.sigmaStarCoarse U a - HCPolySupport.matTranspose (HCPolySupport.Book.Ch02.kappaCoarse U a)

theorem HCPolySupport.Book.Ch02.bCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : bCoarse U a = bCoarse U b

The canonical derived matrix b(U; a) is invariant under a.e. changes of coefficient representative.

theorem HCPolySupport.Book.Ch02.aCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : aCoarse U a = aCoarse U b

The canonical derived matrix a(U; a) is invariant under a.e. changes of coefficient representative.

theorem HCPolySupport.Book.Ch02.aStarCoarse_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : aStarCoarse U a = aStarCoarse U b

The canonical derived matrix aStar(U; a) is invariant under a.e. changes of coefficient representative.