OAI/MathematicalPhysics/PEPSSubvolume/GeometricLower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform geometric-buffer entropy lower bounds.

  1. def OAI.PolynomialPEPS.Subvolume.GeometricLower.blocks line 30
  2. def OAI.PolynomialPEPS.Subvolume.GeometricLower.bufferConstant line 32
  3. lemma OAI.PolynomialPEPS.Subvolume.GeometricLower.blocks_large line 34
  4. lemma OAI.PolynomialPEPS.Subvolume.GeometricLower.rectangle_boundary_weight line 40
  5. lemma OAI.PolynomialPEPS.Subvolume.GeometricLower.rectangle_unique_split line 49
  6. lemma OAI.PolynomialPEPS.Subvolume.GeometricLower.buffer_energy line 56
  7. theorem OAI.PolynomialPEPS.Subvolume.GeometricLower.rectangle_optimizer_entropy_lower line 79