OAI/NumberTheory/CubicMoment/Theta/CubicThetaAngularFrequency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The signed angular multipliers are precisely powers of the actual complex Fourier frequency and its conjugate.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_div_nine line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequency_phase line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaFrequency_conj_phase line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaAngularCoefficient_nat line 47
  5. lemma OAI.CubicFirstMoment.cubicThetaAngularCoefficient_neg_nat line 52
  6. lemma OAI.CubicFirstMoment.cubicThetaAngularCoefficient_nat_succ line 58
  7. lemma OAI.CubicFirstMoment.cubicThetaAngularCoefficient_neg_nat_succ line 64