OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedTorus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The continuous inverted-cusp Fourier series and its physical mean. The constant term is obtained by an actual torus projection.

  1. def OAI.CubicFirstMoment.cubicThetaInvertedTorusRemainder line 19
  2. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorusRemainder_summable line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaInvertedNonzeroTerm_phase line 30
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorusRemainder_real line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorusRemainder_coefficient line 53
  6. def OAI.CubicFirstMoment.cubicThetaInvertedTorus line 69
  7. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorus_real line 74
  8. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorus_mean line 84
  9. theorem OAI.CubicFirstMoment.cubicThetaInverted_horizontal_mean line 96