OAI/NumberTheory/CubicMoment/Decomposition/StoppedDistinguishedLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform log-X saving for the literal distinguished role. Polynomial exclusions and the complementary roughness condition are derived from their actual norm bounds, rather than added prime-row assumptions.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_distinguished_log_saving line 16