OAI/NumberTheory/CubicMoment/Decomposition/StoppedCubeModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual early-stopped cube series has the full squared model, including the controlled shared-prime pairs, with arbitrary log saving.

  1. theorem OAI.CubicFirstMoment.stopped_cube_model_log_saving line 16