OAI/NumberTheory/CubicMoment/Decomposition/StoppedBinDecomposition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact long-bin decomposition of a stopped coefficient. The complementary short-bin part is supported on genuinely smooth integers.

  1. def OAI.CubicFirstMoment.stoppedShortBinTest line 12
  2. def OAI.CubicFirstMoment.stoppedLongBins line 17
  3. lemma OAI.CubicFirstMoment.stoppedBeta_product_predicate line 20
  4. lemma OAI.CubicFirstMoment.largestPrimeChoice_valid_bin line 38
  5. theorem OAI.CubicFirstMoment.stoppedBeta_long_bin_decomposition line 54
  6. theorem OAI.CubicFirstMoment.stopped_short_bin_smooth line 99