OAI/Probability/InvariantIsing/Cavity/CavityPhysicalCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full special coordinates are already coordinates of the base spin: the special frame has zero rows at all cavity sites.

  1. theorem OAI.InvariantIsing.cavity_physical_special_coordinates line 15
  2. theorem OAI.InvariantIsing.cavity_coupled_special_coordinates line 53