OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed logarithmic square-divisor cutoff satisfies the explicit small-divisor power condition at every polynomial stopped length.

  1. lemma OAI.CubicFirstMoment.stopped_logarithmic_divisor_small line 11