OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed divisor cutoff preserves the hybrid sieve range when the frequency length is at most the three-fifths power of the coefficient length.

  1. lemma OAI.CubicFirstMoment.stopped_divisor_cutoff_geometry line 11