OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalAffine.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Affine translates have the same cell integral after an integral nonzero Eisenstein dilation. This is used for the character branches.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontal_multiply_periodic line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaHorizontal_affine_integral line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaHorizontal_affine_integrable line 33