OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralAngularLargeTupleOrdinaryHigh.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_actual line 17