OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialNonzero.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed radial test is nontrivial: its value at s=2 is strictly positive. This supplies a genuine analytic denominator for continuation.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadialTest_kernel_real line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_test_re_pos line 19
  3. theorem OAI.CubicFirstMoment.cubicThetaFourierRadialTest_nonzero line 44