OAI/NumberTheory/CubicMoment/Angular/AngularStoppedCubeModel.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.angular_stopped_cube_model_log_saving line 21