OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual finite Fourier averages at the cube modulus, on sections and on their completed domain space.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFiniteFourier line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFiniteFourier_apply line 21
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2 line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_apply line 44
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_finite line 60
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_norm_le line 70