OAI/NumberTheory/CubicMoment/Decomposition/StoppedSelectedDistinguished.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The selected-divisor role with the actual distinguished-tuple coefficient. Its roughness and coefficient bound are proved internally.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_selected_distinguished_saving line 15