Diagonal

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Block diagonality of the annealed cutoff block matrix

ABK26, e.homs.defs.U.diag. Once the annealed coupling matrix vanishes (e.annealed.khom.zero), the display records that bhom_m(U) = shom_m(U) and that the annealed doubled matrix is block diagonal, bfAhom_m(U) = ((shom_m(U), 0), (0, shom_{m,*}^{-1}(U))).

In CoarseGraining's naming the finite-volume annealed blocks of bfAhom_m(U) = E[bfA_m(U)] are Ch04.annealedB (upper left bhom_m(U)), Ch04.annealedSigmaStarInv (lower right shom_{m,*}^{-1}(U)) and Ch04.annealedSigma (shom_m(U)), with the two mixed blocks -(khom_m^t shom_{m,*}^{-1})(U) and -(shom_{m,*}^{-1} khom_m)(U) sitting in upperRight and lowerLeft.

Main results

• coefficientCutoffLaw_annealedSigma_eq_annealedB
• coefficientCutoffLaw_annealedBlockMatrix_eq_blockDiag
• coefficientCutoffLaw_annealedBlockMatrixAtScale_eq_blockDiag

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedSigma_eq_annealedB {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.annealedSigma (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q) = HCPolySupport.Book.Ch04.annealedB (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q)

ABK26, bhom_m(U) = shom_m(U). The annealed conductivity of the genuine cutoff equals its annealed upper-left block.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrix_eq_blockDiag {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.annealedBlockMatrix (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q) = HCPolySupport.Book.Ch02.blockDiag (HCPolySupport.Book.Ch04.annealedSigma (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q)) (HCPolySupport.Book.Ch04.annealedSigmaStarInv (Cutoff.coefficientCutoffLaw M m) (HCPolySupport.cubeSet Q))

ABK26, e.homs.defs.U.diag. The annealed doubled block matrix of the genuine coefficient cutoff is block diagonal on every triadic cube, with diagonal blocks shom_m(U) and shom_{m,*}^{-1}(U).

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrixAtScale_eq_blockDiag {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n = HCPolySupport.Book.Ch02.blockDiag (HCPolySupport.Book.Ch04.annealedSigmaAtScale (Cutoff.coefficientCutoffLaw M m) n) (HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale (Cutoff.coefficientCutoffLaw M m) n)

Origin-cube form of coefficientCutoffLaw_annealedBlockMatrix_eq_blockDiag.