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

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

Deterministic identities for Chapter 2 observables

This file is the public Chapter 2 owner for deterministic identities among the scalar response, doubled mu, and block response observables. Chapter 4 may turn these identities into law-relative measurability statements; it should not reprove the deterministic algebra.

theorem HCPolySupport.Book.Ch02.doubledMu_eq_Mu {d : ℕ} (U : Domain d) (a : CoeffOn U) (P : BlockVec d) : doubledMu U a P = Mu U.carrier P a.toCoeffField

The public doubled-mu infimum agrees with the deterministic block Mu on the same Chapter 2 domain. This bridge belongs with the deterministic old-engine identities rather than the clean doubled-Mu theorem surface.

theorem HCPolySupport.Book.Ch02.responseJ_eq_doubledMu_neg_left_sub_vecDot {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : responseJ U a p q = doubledMu U a (-p, q) - vecDot p q

The scalar response is the doubled mu value at (-p, q), up to the deterministic pairing term.

theorem HCPolySupport.Book.Ch02.ResponseJ_eq_Mu_neg_left_sub_vecDot {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : ResponseJ U.carrier p q a.toCoeffField = Mu U.carrier (-p, q) a.toCoeffField - vecDot p q

Old-engine scalar response equals old-engine Mu at (-p, q), up to the deterministic pairing term.

theorem HCPolySupport.Book.Ch02.ResponseJ_cubeSet_eq_Mu_neg_left_sub_vecDot {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (p q : Vec d) : ResponseJ (cubeSet Q) p q a.toCoeffField = Mu (cubeSet Q) (-p, q) a.toCoeffField - vecDot p q

Cube-set form of ResponseJ_eq_Mu_neg_left_sub_vecDot.

theorem HCPolySupport.Book.Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum {d : ℕ} (U : Domain d) (a : CoeffOn U) (p pStar q qStar : Vec d) : doubledResponseJ U a (p, q) (qStar, pStar) = 1 / 2 * responseJ U a (p - pStar) (qStar - q) + 1 / 2 * responseJ U a.transpose (pStar + p) (qStar + q)

Public scalar splitting for doubled response.

theorem HCPolySupport.Book.Ch02.doubledResponseJ_eq_BlockJ_of_isEllipticFieldOn {d : ℕ} (U : Domain d) (a : CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (P Q : BlockVec d) : doubledResponseJ U a P Q = BlockJ U.carrier P Q a.toCoeffField

Public bridge from doubled response to the old-engine BlockJ, under the pointwise ellipticity hypothesis required by the old block response space.

theorem HCPolySupport.Book.Ch02.BlockJ_eq_half_ResponseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} (U : Domain d) (a : CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p pStar q qStar : Vec d) : BlockJ U.carrier (p, q) (qStar, pStar) a.toCoeffField = 1 / 2 * ResponseJ U.carrier (p - pStar) (qStar - q) a.toCoeffField + 1 / 2 * ResponseJ U.carrier (pStar + p) (qStar + q) (adjointCoeffField a.toCoeffField)

Old-engine BlockJ is the half-sum of the scalar responses for a and its adjoint.

theorem HCPolySupport.Book.Ch02.BlockJ_cubeSet_eq_half_ResponseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (hEll : IsEllipticFieldOn a.lam a.Lam (openCubeSet Q) a.toCoeffField) (p pStar q qStar : Vec d) : BlockJ (cubeSet Q) (p, q) (qStar, pStar) a.toCoeffField = 1 / 2 * ResponseJ (cubeSet Q) (p - pStar) (qStar - q) a.toCoeffField + 1 / 2 * ResponseJ (cubeSet Q) (pStar + p) (qStar + q) (adjointCoeffField a.toCoeffField)

Cube-set form of the deterministic BlockJ half-sum identity.