OAI/MathematicalPhysics/PEPSSubvolume/TilingEntropy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite submodular covers and tile entropy summation.

  1. def OAI.PolynomialPEPS.SubvolumeTiling.unionTiles line 27
  2. theorem OAI.PolynomialPEPS.SubvolumeTiling.unionTiles_empty line 30
  3. theorem OAI.PolynomialPEPS.SubvolumeTiling.unionTiles_insert line 31
  4. theorem OAI.PolynomialPEPS.SubvolumeTiling.subset_unionTiles line 35
  5. theorem OAI.PolynomialPEPS.SubvolumeTiling.unionTiles_mono line 39
  6. theorem OAI.PolynomialPEPS.SubvolumeTiling.disjoint_unionTiles line 46
  7. theorem OAI.PolynomialPEPS.SubvolumeTiling.condition_on_past line 51
  8. theorem OAI.PolynomialPEPS.SubvolumeTiling.selected_tiles line 69
  9. theorem OAI.PolynomialPEPS.SubvolumeTiling.tiles_subadditive line 94
  10. theorem OAI.PolynomialPEPS.SubvolumeTiling.selected_color line 109
  11. theorem OAI.PolynomialPEPS.SubvolumeTiling.color_average line 134
  12. theorem OAI.PolynomialPEPS.SubvolumeTiling.color_recurrence line 163