OAI/NumberTheory/CubicMoment/Theta/CubicThetaRemainderWeights.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A summable majorant on the actual Fourier lattice, with its full mass bounded.

  1. def OAI.CubicFirstMoment.cubicThetaPrimaryDerivativeWeight line 12
  2. def OAI.CubicFirstMoment.cubicThetaRamifiedDerivativeWeight line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimaryDerivativeWeight_nonneg line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaRamifiedDerivativeWeight_nonneg line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimaryDerivativeWeight_mass line 34
  6. lemma OAI.CubicFirstMoment.cubicThetaRamifiedDerivativeWeight_mass line 43
  7. def OAI.CubicFirstMoment.cubicThetaPositiveRemainderWeight line 52
  8. def OAI.CubicFirstMoment.cubicThetaNegativeRemainderWeight line 56
  9. def OAI.CubicFirstMoment.cubicThetaHighRemainderWeight line 60
  10. def OAI.CubicFirstMoment.cubicThetaRemainderWeight line 64
  11. lemma OAI.CubicFirstMoment.cubicThetaRemainderWeight_properties line 68