OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveModelL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal arithmetic series in the L2 space of every positive height strip, with its scalar still retained.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_point_continuous line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_positive_memLp line 25
  3. def OAI.CubicFirstMoment.cubicThetaPositiveModelStrip line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourierWeight_memLp line 41
  5. def OAI.CubicFirstMoment.cubicThetaPositiveStripFourierTest line 56