Coarse-graining support: #
Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.TraceBudgetAlgebra
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedBlockJTraceAverage_eq_blockJTraceAverageWithNormalizers
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
(a : RegCoeffField d)
:
have b := hP.barSigmaAtScale hStruct center;
have c := hP.barSigmaStarAtScale hStruct center;
have S := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c);
have T := Matrix.diagonal (scalarFullBlockSqrtDiag b c);
normalizedBlockJTraceAverage hP hStruct center Q j a = blockJTraceAverageWithNormalizers S T Q j a
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.blockJTraceAverageWithNormalizers_eq_traceBudget_descendantsAverageBlockMat
{d : ℕ}
[NeZero d]
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
(S T : FullBlockMat d)
(Q : TriadicCube d)
(j : ℕ)
:
blockJTraceAverageWithNormalizers S T Q j a = fullBlockJTraceBudgetWithNormalizers S T
(descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun)
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockJTraceBudgetWithNormalizers_normalized_eq_trace
{d : ℕ}
{b c : ℝ}
(hb : 0 < b)
(hc : 0 < c)
(A : BlockMat d)
:
have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c);
have T := Matrix.diagonal (scalarFullBlockSqrtDiag b c);
have θ := b * c⁻¹;
fullBlockJTraceBudgetWithNormalizers D T A = (1 + θ) / 2 * Ch02.fullBlockTrace (D * toFullBlockMat A * D) - ↑(Fintype.card (BlockCoord d))
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationMatrix_eq_diagonal_average_sub_annealed
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
(a : RegCoeffField d)
:
have b := hP.barSigmaAtScale hStruct center;
have c := hP.barSigmaStarAtScale hStruct center;
have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c);
descendantsAverageNormalizedFluctuationMatrix hP hStruct center Q j a = D * (toFullBlockMat
(descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun) - toFullBlockMat (Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center)) * D