OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootFourierL2.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual finite Fourier projections on the completed root-cover space, with their exact agreement on square-integrable sections.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteFourier line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteFourier_apply line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFiniteFourier_val line 33
  4. def OAI.CubicFirstMoment.cubicThetaPrimeRootFourierL2 line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFourierL2_apply line 54
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootFourierL2_finite line 68
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootFourierL2_idempotent line 77