OAI/NumberTheory/CubicMoment/Angular/AngularStoppedMixedLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The corrected mixed-term error for the actual stopped coefficient. The product-squarefree model is retained; the remaining model-coprimality comparison belongs to the variance assembly.

  1. theorem OAI.CubicFirstMoment.angular_stopped_corrected_mixed_log_saving line 24