OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspLatticeWeight.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The summable lattice weight controlling both values and first spatial derivatives of the arithmetic remainder in each cusp.

  1. def OAI.CubicFirstMoment.cubicThetaCuspLatticeWeight line 11
  2. def OAI.CubicFirstMoment.cubicThetaCuspLatticeMass line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspLatticeWeight_nonneg line 17
  4. def OAI.CubicFirstMoment.pairWeight line 22
  5. def OAI.CubicFirstMoment.rowIndex line 25
  6. lemma OAI.CubicFirstMoment.rowIndex_injective line 28
  7. lemma OAI.CubicFirstMoment.pairWeight_summable line 33
  8. lemma OAI.CubicFirstMoment.cubicThetaCuspLatticeWeight_summable line 38
  9. lemma OAI.CubicFirstMoment.cubicThetaCuspLatticeWeight_tsum_le line 43