OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unique indexing of the primary theta frequencies by the original squarefree and cube variables. There is no multiplicity factor.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimaryPair line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimaryNumerator line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimaryNumerator_support line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimaryNumerator_injective line 22
  5. def OAI.CubicFirstMoment.cubicThetaPrimaryIndexEquiv line 31
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimary_tsum line 40

    Source documentation

    Reindex a theta sum over S with exactly one term for each primary squarefree-times-cube pair.

    theorem cubicThetaPrimary_tsum (f : Eisenstein → ℂ) :
    (∑' n : Eisenstein, if cubicThetaPrimarySupport n then f n else 0) =
      ∑' cd : CubicThetaPrimaryPair, f (cubicThetaPrimaryNumerator cd) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaPrimarySupport, OAI.CubicFirstMoment.CubicThetaPrimaryPair, OAI.CubicFirstMoment.cubicThetaPrimaryNumerator