OAI/Analysis/LipschitzHilbert/Packets/PacketDataLatticeSites.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The physical sites are exactly the translated sheared lattices used by the common probability average.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.actualSite_eq_lattice_translate line 13