OAI/NumberTheory/CubicMoment/Estimates/LargeTupleOrdinaryHigh.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual high boxes having an ordinary surviving tuple. A single fixed group works for the entire box, and constants are uniform over the finite set of possible groups. The original sharp cutoff is retained.

  1. theorem OAI.CubicFirstMoment.largePrimeTuplePiece_ordinary_high_log_saving line 16