OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSequenceSW.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete Kummer sequence condition for the literal stopped coefficient: exact long/short splitting, both largest-prime roles, all bin costs, and the smooth remainder are derived.

  1. theorem OAI.CubicFirstMoment.angular_stopped_sequence_kummer_sw line 20