OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspPotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The nonzero Fourier-mode potential confines mass high in the cusp. This is the uniform tail estimate for the logarithmic radial model.

  1. lemma OAI.CubicFirstMoment.cubicThetaRowHeatScale_lower_bound line 12
  2. lemma OAI.CubicFirstMoment.potential_integrable line 17
  3. lemma OAI.CubicFirstMoment.cubicTheta_potential_tail line 27
  4. theorem OAI.CubicFirstMoment.cubicTheta_nonzero_mode_tail line 55