OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanExactEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact energy and loss of the finite Kloosterman operator. The loss is the Fourier energy outside the primary unit classes, with no analytic estimate or local representation hypothesis.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight_norm_sq line 15
  2. theorem OAI.CubicFirstMoment.cubicThetaWeightedResidueInversion_energy line 22
  3. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanApply_energy line 41
  4. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanApply_loss line 50