OAI/NumberTheory/CubicMoment/Estimates/SparseStoppedModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual late-stop squarefree model is power-saving by direct counting and the two proved coefficient energies.

  1. theorem OAI.CubicFirstMoment.ordinary_late_stopped_model line 14