OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedUniform.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the literal stopped distinguished coefficient on the fixed X-envelope. The bin boundary parameter does not enter them.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_distinguished_uniform line 14