OAI/MathematicalPhysics/PEPSSubvolume/Subvolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strict subvolume exponent from uniform square-scale recurrence.

  1. theorem OAI.PolynomialPEPS.Subvolume.SubvolumeArithmetic.power_bound line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.RectangleTiling.uniform_subvolume_square line 71