OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeFourierOrbit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal positive-cutoff source orbit under prime-cube dilation.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeFourierOrbit line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeFourierOrbit_zero line 23
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeFourierOrbit_step line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeFourierOrbit_square_start line 73