OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveModelObservation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit nonconstant arithmetic model gives every positive-height Fourier test of the actual residue, not only its high-cusp restriction.

  1. theorem OAI.CubicFirstMoment.cubicThetaPositiveNormalized_nonzero_observation line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaPositiveModel_nonzero_observation line 28
  3. theorem OAI.CubicFirstMoment.cubicThetaPositiveNormalized_zero_observation line 44
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveModel_zero_observation line 57
  5. theorem OAI.CubicFirstMoment.cubicThetaPositiveModel_all_observations line 84