OAI/NumberTheory/CubicMoment/Decomposition/StoppedSelectedRow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The selected-bin free-prime row with its actual full product, complementary exclusion and both stopping tests.

  1. def OAI.CubicFirstMoment.stoppedSelectedPrimeSet line 12
  2. def OAI.CubicFirstMoment.stoppedSelectedPrimeRow line 21
  3. lemma OAI.CubicFirstMoment.stoppedSelectedPrimeSet_primary line 26
  4. theorem OAI.CubicFirstMoment.stopped_selected_prime_row_saving line 32