OAI/Analysis/LipschitzHilbert/Packets/PacketDataInteractionGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The short family used in the selected-tree argument is defined by actual nonzero Gram interactions. Its angular geometry follows from the packet spectra, rather than being a separate analytic premise.

  1. def OAI.LipschitzHilbert.PacketLatticeData.interactingShortPackets line 19
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.interactingShortPackets_subset line 24
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.interacting_short_length line 27
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.interacting_short_direction line 33
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.interacting_short_margin line 52