OAI/MathematicalPhysics/PEPSFilters/SiteBlocks.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Matrix blocks and bounded single-site factors for two-site operators.

  1. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.injectionMatrix line 28
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.injectionMatrix_star_mul line 31
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.injectionMatrix_norm_le line 38
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.matrix_block_apply line 45
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.matrix_block_norm_le line 49
  6. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.reindexStarAlgEquiv line 61
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.norm_reindex line 66
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.matrix_single_norm_le line 70
  9. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteConfigurationEquiv line 92
  10. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal line 103
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal_supported line 106
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal_norm line 109
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal_apply line 113
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal_mul_apply line 118
  15. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairConfiguration line 161
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairConfiguration_left line 164
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairConfiguration_right line 167
  18. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairConfigurationEquiv line 170
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairConfiguration_restrict line 184
  20. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairBlock line 194
  21. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.pairBlock_norm_le line 197
  22. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.two_site_decomposition line 208
  23. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.siteLocal_inside line 231
  24. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.exists_two_site_crossing_factors line 241