OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarCuspQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scaled scalar cusp cutoffs descend to the actual quotient in every arithmetic cusp, using normality of the principal group.

  1. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_norm line 14
  2. def OAI.CubicFirstMoment.cubicThetaScalarCuspAt line 29
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspAt_invariant line 32
  4. def OAI.CubicFirstMoment.cubicThetaScalarCuspQuotient line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspQuotient_apply line 45
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspQuotient_continuous line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspQuotient_norm line 63