OAI/NumberTheory/CubicMoment/Theta/CubicThetaSievePhase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The additive character that detects the primary cubic theta support. It is computed from the actual lambda^-4 frequency lattice.

  1. def OAI.CubicFirstMoment.cubicThetaSievePhase line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_add line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_neg line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_ramified line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_lambda line 43
  6. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_primary line 67
  7. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_negative_primary line 75
  8. lemma OAI.CubicFirstMoment.cubicThetaSievePhase_high line 84

    Source documentation

    Every supported coefficient of ramified order at least three has the trivial detector phase.

    lemma cubicThetaSievePhase_high {n : Eisenstein} (R : CubicThetaCoordinates n)
    (hk : 3 ≤ R.order) : cubicThetaSievePhase n = 1 := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.CubicThetaCoordinates, OAI.CubicFirstMoment.cubicThetaSievePhase