OAI/NumberTheory/CubicMoment/Angular/AngularUniformHighStoppedTail.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.angular_high_stopped_envelope_tail_uniform line 14