OAI/NumberTheory/CubicMoment/Estimates/UpperLowTailUniform.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The upper low-scale estimate permits any sufficiently small positive stopping exponent. This makes the stopping choice compatible with the prime high-row estimate.

  1. theorem OAI.CubicFirstMoment.upperStoppedTail_bound_uniform line 14
  2. theorem OAI.CubicFirstMoment.upperStoppedEnvelopeTail_bounds_uniform line 113
  3. theorem OAI.CubicFirstMoment.upperStoppedFilteredArity_bounds_uniform line 145
  4. theorem OAI.CubicFirstMoment.upperStoppedFilteredTail_isLittleO_uniform line 180
  5. theorem OAI.CubicFirstMoment.upperLowTail_isLittleO_uniform line 210