OAI/NumberTheory/CubicMoment/Decomposition/StoppingBinShift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact transport between geometric bins with two ambient norm cutoffs. Below the smaller cutoff the bin labels differ by one fixed integer, and the corresponding lower endpoints and prefix sets agree.

  1. lemma OAI.CubicFirstMoment.geometricBinCount_mono line 13
  2. lemma OAI.CubicFirstMoment.geometricPrimeBin_shift line 19
  3. lemma OAI.CubicFirstMoment.geometricBinLower_shift line 33
  4. lemma OAI.CubicFirstMoment.geometricPrimeBin_finset_shift line 42
  5. lemma OAI.CubicFirstMoment.geometricPrimeBin_prefix_shift line 55
  6. lemma OAI.CubicFirstMoment.geometricPrimeSurrogate_shift line 68
  7. lemma OAI.CubicFirstMoment.geometricStoppingPrimeSetTest_shift line 78
  8. lemma OAI.CubicFirstMoment.geometricStoppedSideTest_shift line 100