OAI/Analysis/LipschitzHilbert/Trees/SourceInteractionGeometry.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.SourceLabeledLattice.interactingShortPackets line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.interactingShortPackets_subset line 23
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.interacting_short_length line 26
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.interacting_short_direction line 32
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.interacting_short_margin line 51