OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarCuspCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The unphased, scaled incoming cutoff is an actual invariant scalar. Its arithmetic sum is locally finite at all scales at least one.

  1. def OAI.CubicFirstMoment.cubicThetaScalarCuspTerm line 12
  2. def OAI.CubicFirstMoment.cubicThetaScalarCusp line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspTerm_zero line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaScalarCuspTerm_high line 22
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_finite line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_compact_sum line 36
  7. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_smooth line 46
  8. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_invariant line 59
  9. lemma OAI.CubicFirstMoment.cubicThetaScalarCusp_high line 67