OAI/NumberTheory/CubicMoment/Decomposition/StoppedPrimePredicate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Both actual stopping branches, including failure of the earlier crossing test. Fixing the selected prime's bin fixes all these tests.

  1. def OAI.CubicFirstMoment.stoppedSideTest line 12
  2. lemma OAI.CubicFirstMoment.stoppedSideTest_free_prime_same_bin line 17
  3. theorem OAI.CubicFirstMoment.sum_stoppedSide_same_bin line 29
  4. theorem OAI.CubicFirstMoment.stoppedSideTest_free_distinguished_interval line 52