Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.TraceAveragePackaging

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.blockJTraceAverageWithNormalizers_eq_sum_descendantsAverage {d : ℕ} (S T : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : blockJTraceAverageWithNormalizers S T Q j a = ∑ α : BlockCoord d, descendantsAverage Q j fun (R : TriadicCube d) => blockJObservableCubeSetBlockVec R (fullBlockMatrixProbe S α) (fullBlockMatrixProbe T α) a

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.integral_blockJTraceAverageWithNormalizers_eq_sum_originCube_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (child parent : ℕ) (hchild_parent : child ≤ parent) (S T : FullBlockMat d) : ∫ (a : RegCoeffField d), blockJTraceAverageWithNormalizers S T (originCube d ↑parent) (parent - child) a ∂P = ∑ α : BlockCoord d, Ch04.expectedBlockJCubeSet P (originCube d ↑child) (fullBlockMatrixProbe S α).1 (fullBlockMatrixProbe T α).2 (fullBlockMatrixProbe S α).2 (fullBlockMatrixProbe T α).1