OAI/Analysis/LipschitzHilbert/Geometry/SourceSelectedFarBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The far contribution belonging to one actual recorded positive selection top. The required short-packet packing follows from a combination of selection order and the original Fourier margins.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_selected_far_gram_bound line 17