OAI/NumberTheory/CubicMoment/Estimates/UniformHighStoppedTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform power width for actual stopped coefficients, chosen before both their arity-dependent bound and the desired logarithmic saving.

  1. theorem OAI.CubicFirstMoment.high_stopped_envelope_tail_uniform line 13