OAI/NumberTheory/CubicMoment/Decomposition/StoppedSelectedCollection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the selected-bin free-prime rows, and the complementary norm cutoff forced by the lower endpoint of the prime bin.

  1. lemma OAI.CubicFirstMoment.stoppedSelectedPrimeSet_subset line 12
  2. lemma OAI.CubicFirstMoment.selectedStopped_row_collection line 19
  3. lemma OAI.CubicFirstMoment.selectedStopped_complement_bound line 43
  4. lemma OAI.CubicFirstMoment.selectedStopped_row_eq_zero line 65
  5. theorem OAI.CubicFirstMoment.selectedStopped_original_rows line 76