OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmetic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The normalized arithmetic coefficient of DR v3 (5.7), indexed on the common cusp lattice lambda^-4 Z[omega]. The coefficient used in the Whittaker series is tau(mu)/|mu|. No modular transformation is asserted.

  1. structure OAI.CubicFirstMoment.CubicThetaCoordinates line 13
  2. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.ne_zero line 23
  3. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.unique line 28
  4. def OAI.CubicFirstMoment.cubicThetaUnitPhase line 41

    Source documentation

    Unit phases in the first three cases of (5.7). Raising a sixth root of unity to the fourth power removes its sign.

    def cubicThetaUnitPhase (u : Eisensteinˣ) : ℂ :=
…
  5. lemma OAI.CubicFirstMoment.cubicThetaUnitPhase_norm line 46
  6. def OAI.CubicFirstMoment.cubicThetaTwistedGauss line 51

    Source documentation

    The normalized Gauss sum at an invertible additive frequency.

    def cubicThetaTwistedGauss (c α : Eisenstein) : ℂ := star (cubicSymbol c α)*gauss c

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.gauss

  7. lemma OAI.CubicFirstMoment.cubicThetaTwistedGauss_norm_le line 53
  8. def OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude line 58
  9. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude_nonneg line 61
  10. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude_le line 66
  11. def OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient line 80
  12. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_norm_le line 88
  13. def OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient line 101
  14. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_formula line 106

    Source documentation

    Uniqueness makes the explicit formula independent of the chosen coordinate witness.

    lemma cubicThetaArithmeticCoefficient_formula {n : Eisenstein} (R : CubicThetaCoordinates n) :
    cubicThetaArithmeticCoefficient n = R.coefficient := by
…

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

  15. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_norm_le line 111
  16. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_bound line 118
  17. theorem OAI.CubicFirstMoment.cubicThetaArithmetic_summable line 124

    Source documentation

    Absolute convergence for the literal normalized arithmetic coefficients.

    theorem cubicThetaArithmetic_summable {v : ℝ} (hv : 0 < v) (z : ℂ) :
    Summable (cubicThetaSeriesTerm cubicThetaArithmeticCoefficient z v) :=
…

    Mentions: OAI.CubicFirstMoment.cubicThetaSeriesTerm, OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient