OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedConstantCoefficient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Nontrivial translated cusps have zero constant coefficient. This is deduced from the exact finite Gauss support, not assumed as a cusp condition.

  1. lemma OAI.CubicFirstMoment.cubicThetaShiftedZero_observation_germ line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedZero_window_pairing line 37
  3. theorem OAI.CubicFirstMoment.cubicThetaShiftedConstantCoefficient_zero line 54
  4. lemma OAI.CubicFirstMoment.cubicThetaShifted_nontrivial_constant line 81
  5. theorem OAI.CubicFirstMoment.cubicThetaShiftedConstantCoefficient_nontrivial line 97