OAI/NumberTheory/CubicMoment/Estimates/UpperStoppedSuffix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The upper portion of the actual stopped height sum is an aligned full tail. This preserves cancellation when the ordinary heights are removed.

  1. def OAI.CubicFirstMoment.upperStoppedWindow line 13
  2. def OAI.CubicFirstMoment.upperStoppedFilteredArity line 18
  3. lemma OAI.CubicFirstMoment.upperStoppedWindow_sum line 23
  4. lemma OAI.CubicFirstMoment.upperStoppedFilteredArity_suffix line 35
  5. theorem OAI.CubicFirstMoment.upperStoppedFilteredArity_bounds line 45
  6. theorem OAI.CubicFirstMoment.upperStoppedFilteredTail_isLittleO line 75