OAI/MathematicalPhysics/PEPSFilters/GridCollar.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Separated rectangular contours and lattice perimeter bounds.

  1. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.enlargedRectangle line 26
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.mem_enlargedRectangle line 30
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.enlargedRectangle_monotone line 35
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.adjacent_mem_enlargedRectangle line 40
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossing_enlargedRectangle_unique line 52
  6. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.rectangle_contours_separated line 72
  7. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.exists_rectangle_maximizer_energy line 79
  8. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.horizontalBand line 99
  9. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.verticalBand line 103
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.horizontalBand_card_le line 107
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.verticalBand_card_le line 142
  12. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossingCount_enlargedRectangle line 175
  13. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossingCount_enlargedRectangle_scale line 213