OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveStripHorizontalDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact radial tests recover the horizontal Fourier coefficient of an arbitrary cusp L2 vector at almost every height.

  1. def OAI.CubicFirstMoment.cubicThetaPositiveStripHorizontalDensity line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripHorizontalDensity_integrable line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveStripHorizontalDensity_pairing line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveStripHorizontalDensity_zero line 52