OAI/NumberTheory/CubicMoment/Theta/CubicThetaCirclePolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite Fourier polynomial underlying higher angular extraction. Its highest Fourier mode is a pure power of the complex frequency.

  1. def OAI.CubicFirstMoment.cubicThetaCirclePower line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaCircle_fourier_pow line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaCirclePower_expansion line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaCirclePower_coefficient line 41
  5. lemma OAI.CubicFirstMoment.cubicThetaCirclePower_coefficient_above line 59
  6. lemma OAI.CubicFirstMoment.cubicThetaCirclePower_coefficient_top line 68