OAI/MathematicalPhysics/PEPSSubvolume/LocalBlocks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Local matrix-unit blocks with operator norm bounds.

  1. def OAI.PolynomialPEPS.Subvolume.LocalBlocks.column line 25
  2. def OAI.PolynomialPEPS.Subvolume.LocalBlocks.block line 28
  3. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.column_gram line 31
  4. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.column_norm_le line 36
  5. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.block_eq line 44
  6. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.block_norm_le line 50
  7. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.block_decomposition line 63
  8. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.single_norm_le line 68
  9. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.decomposition_cost line 84
  10. def OAI.PolynomialPEPS.Subvolume.LocalBlocks.reindexStarAlgEquiv line 103
  11. lemma OAI.PolynomialPEPS.Subvolume.LocalBlocks.norm_reindex line 107