OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedWindowFourier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact initial Fourier observation on a finite translated-cusp window.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedWindowRadialTest line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowObservation_normalized line 16