OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSelectedCollection.lean

GitHub source file

3 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.angular_selectedStopped_row_collection line 15
  2. lemma OAI.CubicFirstMoment.angular_selectedStopped_row_eq_zero line 40
  3. theorem OAI.CubicFirstMoment.angular_selectedStopped_original_rows line 52