OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoefficientEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact squared sizes of the theta coefficients, for normalization by their Fourier energy. The zero classes remain in the formula.

  1. lemma OAI.CubicFirstMoment.cubicThetaTwistedGauss_unit_lambda_norm line 10
  2. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_norm line 22
  3. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude_sq line 37
  4. theorem OAI.CubicFirstMoment.cubicThetaNormalizedCoefficient_energy line 47