OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A bounded global observation of the inverted Eisenstein series. The literal strip integral is evaluated by the previously proved physical mean.

  1. def OAI.CubicFirstMoment.cubicThetaInvertedWindowTest line 14
  2. def OAI.CubicFirstMoment.cubicThetaInvertedWindowObservable line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaInvertedWindowObservable_meromorphic line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedWindowObservable_right line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaInvertedWindow_integrable line 56
  6. lemma OAI.CubicFirstMoment.cubicThetaInvertedWindowObservable_normalized line 71