OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialCompactness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Dirichlet cusp inclusion is compact for each nonzero Fourier potential: local compactness is combined with the uniform exponential tail.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadial_tail_small line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaRadial_cutoff_remainder line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaRadial_unit_cutoff_error line 46
  4. theorem OAI.CubicFirstMoment.cubicThetaRadial_unit_precompact line 64