OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticModelObservation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted Fourier observations identify the arithmetic residue with the explicit coefficient model, retaining its one actual base scalar.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_horizontal line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_pair_integrable line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModel_observation line 43
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticModel_nonzero_observation line 87
  5. theorem OAI.CubicFirstMoment.cubicThetaArithmeticModel_zero_observation line 103
  6. theorem OAI.CubicFirstMoment.cubicThetaArithmeticModel_all_observations line 127