OAI/NumberTheory/CubicMoment/Decomposition/StoppedLongBinSaving.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

All long bins of the literal stopped coefficient have arbitrary logarithmic saving. The number of bins is accounted for explicitly.

  1. def OAI.CubicFirstMoment.stoppedCharacterSum line 17
  2. lemma OAI.CubicFirstMoment.stoppedCharacterSum_largest_roles line 27
  3. theorem OAI.CubicFirstMoment.stoppedBeta_long_bins_log_saving line 42