OAI/NumberTheory/CubicMoment/Decomposition/StoppedSelectedMoment.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.selectedStopped_original_collection line 13
  2. theorem OAI.CubicFirstMoment.stopped_selected_original_saving line 45