OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedTrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite Fourier trace in the ramified correction never vanishes. It equals two on primary frequencies and on lambda cubes.

  1. lemma OAI.CubicFirstMoment.cubicThetaRamifiedPhase_one line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaRamifiedPhase_cube line 22
  3. theorem OAI.CubicFirstMoment.cubicThetaRamifiedTrace_ne_zero line 32
  4. theorem OAI.CubicFirstMoment.cubicThetaRamifiedTrace_primary line 43
  5. theorem OAI.CubicFirstMoment.cubicThetaRamifiedTrace_lambda_cube line 54