OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierProfileNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact mass of a compact cusp Fourier source and its height scaling.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalFourier_character_self line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaFourierProfile_inner_self line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaWeightSquareIntegral_scale line 30
  4. theorem OAI.CubicFirstMoment.cubicThetaFourierProfile_scale_norm_sq line 50