OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveResidueObservation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic normalization of the residue against every positive compact Fourier test. The full low-height incoming correction is entire.

  1. theorem OAI.CubicFirstMoment.cubicThetaPositiveFourierObservable_continued line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaPositiveResidue_fourier_observation line 38