OAI/NumberTheory/CubicMoment/Theta/CubicThetaMassPushforward.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summable nonnegative coordinate masses pushed to the actual Fourier lattice.

  1. def OAI.CubicFirstMoment.cubicThetaMassPushforward line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaMassPushforward_properties line 14