OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual trace character on a small horizontal circle, with both orientations.

  1. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_trace line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_trace_reverse line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_add line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_circle line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_circle_reverse line 52
  6. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_frequency_power line 61
  7. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_conj_frequency_power line 70