OAI/NumberTheory/CubicMoment/Theta/CubicThetaStripHorizontalDensity.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.cubicThetaStripHorizontalDensity line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaStripHorizontalDensity_integrable line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaStripHorizontalDensity_pairing line 39
  4. theorem OAI.CubicFirstMoment.cubicThetaStripHorizontalDensity_zero line 51