OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveStripFubini.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fubini and radial Fourier pairing at any positive cutoff.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveCuspStrip_fubini line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaFourierStripSeed_pair_on_strip line 30
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourierPairing_integrable line 49
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveFourierProfile_pairing_radial line 59
  5. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourier_weight_integrable line 89