OAI/NumberTheory/CubicMoment/Decomposition/NoStopCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Collect the no-stop branch as an actual outer Type-I coefficient. The surrogate test is retained in its original form.

  1. def OAI.CubicFirstMoment.noStopCoefficient line 12
  2. theorem OAI.CubicFirstMoment.noStop_coefficient_collection line 17
  3. theorem OAI.CubicFirstMoment.noStop_coefficient_divisor_bound line 41