OAI/Probability/InvariantIsing/Cavity/CavityFactorBlockProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extraction of cavity coefficients from the full small compression matrix. This lets the proved Haar compression law act on the actual factor coefficients, including the subtracted base diagonal.

  1. def OAI.InvariantIsing.cavityFactorBlocksFromMatrix line 14
  2. lemma OAI.InvariantIsing.continuous_cavityFactorBlocksFromMatrix line 19
  3. lemma OAI.InvariantIsing.cavityFactorBlocksFromMatrix_special line 24
  4. lemma OAI.InvariantIsing.cavitySmallFactorBlocks_reindex line 30
  5. lemma OAI.InvariantIsing.cavityCompressionFactorBlocks_eq_projection line 39