OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralStoppedMixedLogSaving.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.stopped_corrected_mixed_log_saving_actual line 17