OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveStripPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted Fourier pairing on the actual positive strip, and its compatibility with the global energy restriction.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveStrip_inner_formula line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveRestriction_finite_pairing line 62
  3. theorem OAI.CubicFirstMoment.cubicThetaPositiveRestriction_pairing line 85
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveModelStrip_observations line 97