OAI/Analysis/LipschitzHilbert/Geometry/SourceSignedSelectedFarBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The far contribution belonging to one actual recorded signed 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_signed_selected_far_gram_bound line 18