OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedRowWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Zero-extended periodic weights of the translated inverted rows. The finite residue modulus is 3*c in the variable d=3*u.

  1. lemma OAI.CubicFirstMoment.cubicTheta_coprime_add_left line 10
  2. lemma OAI.CubicFirstMoment.cubicTheta_coprime_add_right line 20
  3. def OAI.CubicFirstMoment.cubicThetaShiftedRowWeight line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowWeight_norm line 27
  5. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowWeight_periodic line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowWeight_congr line 49
  7. def OAI.CubicFirstMoment.cubicThetaShiftedResidueWeight line 56
  8. lemma OAI.CubicFirstMoment.cubicThetaShiftedResidueWeight_mk line 59
  9. def OAI.CubicFirstMoment.cubicThetaShiftedGaussCoefficient line 70
  10. lemma OAI.CubicFirstMoment.cubicThetaShiftedGaussCoefficient_norm line 75