OAI/MathematicalPhysics/PEPSSubvolume/RegionSSA.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Physical-region entropy submodularity and buffer bounds.

  1. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.density_between_dual line 30
  2. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.split_tensorLeft line 36
  3. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.split_tensorRight line 45
  4. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.density_ptrR line 54
  5. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.density_ptrL line 63
  6. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.traceEntropy_density line 72
  7. def OAI.PolynomialPEPS.Subvolume.RegionSSA.shellPairEquiv line 83
  8. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.join_three line 102
  9. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.ptrR_reindex_left line 115
  10. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.ptrL_reindex_right line 118
  11. theorem OAI.PolynomialPEPS.Subvolume.RegionSSA.conditional_entropy_antitone line 128
  12. theorem OAI.PolynomialPEPS.Subvolume.GeometricComparison.rectangle_conditional_contraction line 177