OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointC1Trace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The gradient trace identity before integration. Its finite sum uses the same literal representatives and cubic phases as the Hecke trace.

  1. def OAI.CubicFirstMoment.cubicThetaPointC1Trace line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPointC1Trace_apply line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaPointC1Trace_gradient_point line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaPointC1Pair_integrable line 52