OAI/NumberTheory/CubicMoment/Decomposition/StoppedEarlyDivisorMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Noncube cancellation for the full coprimality expansion of the literal early-stopped coefficient. Its coefficient bound and roughness are proved from the actual stopping construction.

  1. theorem OAI.CubicFirstMoment.stopped_early_divisor_noncube_mass line 16