OAI/NumberTheory/CubicMoment/Estimates/HighWideTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width support version of the uniform power-width tail. The same positive exponent is chosen before all coefficient arities and energies.

  1. theorem OAI.CubicFirstMoment.high_wide_envelope_tail_uniform line 13