OAI/NumberTheory/CubicMoment/Angular/AngularStoppedCorrectedDispersion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Corrected dispersion for the actual early-stopped coefficients. The positive variance, its common-factor restoration, the squarefree mass, and the product-squarefree mixed term are all derived arithmetic sums.

  1. theorem OAI.CubicFirstMoment.angular_stopped_corrected_dispersion_log_saving line 23