OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSelectedMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Original selected-side stopped sums, after their exact free-prime reindexing. The complementary cutoff is derived from the actual bin.

  1. theorem OAI.CubicFirstMoment.angular_selectedStopped_original_collection line 17
  2. theorem OAI.CubicFirstMoment.angular_stopped_selected_original_saving line 50