OAI/MathematicalPhysics/PEPSSubvolume/SquareRecurrence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform entropy contraction across square scales.

  1. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.physical_color_recurrence line 33
  2. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.physical_density_contraction line 75
  3. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.tile_as_box line 132
  4. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.box_mul line 138
  5. lemma OAI.PolynomialPEPS.Subvolume.RectangleTiling.unit_box_card line 143
  6. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.physical_three_child_gain line 149
  7. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.square_scale_entropy line 174