OAI/Probability/ClassicalON/AnnulusPartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.LatticeGraph.thetaPotential line 8
2. def OAI.ClassicalON.LatticeGraph.rotatedBoundaryPins line 11
3. theorem OAI.ClassicalON.LatticeGraph.thetaPotential_binary_pins line 15
4. theorem OAI.ClassicalON.LatticeGraph.rotatedBoundaryPins_boundary line 23
5. theorem OAI.ClassicalON.LatticeGraph.rotatePotential_spinSystem line 31
6. theorem OAI.ClassicalON.LatticeGraph.annulus_partition_ratio line 36