OAI/NumberTheory/CubicMoment/Angular/AngularLargeTupleOrdinaryHigh.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.angular_largePrimeTuplePiece_ordinary_high_log_saving line 17