OAI/NumberTheory/CubicMoment/Decomposition/StoppedMixedLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.CubicFirstMoment.stopped_corrected_mixed_log_saving line 20