OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanInvolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The weighted inversion in the actual Kloosterman factorization is self-adjoint; its square is precisely the primary-unit projection.

  1. lemma OAI.CubicFirstMoment.cubicThetaResidueInversePerm_of_isUnit line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaResidueInversePerm_of_not_isUnit line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaResidueInversePerm_twice line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight_not_primary line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight_one line 44
  6. theorem OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight_inverse line 49
  7. theorem OAI.CubicFirstMoment.cubicThetaWeightedResidueInversion_square line 79
  8. theorem OAI.CubicFirstMoment.cubicThetaWeightedResidueInversion_symmetric line 89