OAI/NumberTheory/CubicMoment/Decomposition/StoppedCubeExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cube factors in the frequency are exact exclusions for the literal stopped coefficient. Its established Kummer sequence bound therefore applies to a small noncube core times an arbitrary bounded cube.

  1. theorem OAI.CubicFirstMoment.stoppedCharacterSum_cube line 16
  2. theorem OAI.CubicFirstMoment.stopped_sequence_cube_sw line 33