OAI/NumberTheory/CubicMoment/Angular/AngularStoppedFullModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full small-square-divisor variance model for the literal stopped coefficient, obtained by restoring its actual common-factor rows.

  1. theorem OAI.CubicFirstMoment.angular_stopped_divisor_full_model_log_saving line 19