OAI/NumberTheory/CubicMoment/Decomposition/StoppedFullModel.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.stopped_divisor_full_model_log_saving line 15