OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedWindowTest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded Fourier tests on finite translated-cusp windows.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedFourierWeight line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedFourierWeight_continuous line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowWeight_memLp line 24
  4. def OAI.CubicFirstMoment.cubicThetaShiftedWindowTest line 46
  5. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowTest_integrable line 51
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowTest_pairing line 76
  7. def OAI.CubicFirstMoment.cubicThetaShiftedWindowObservation line 103
  8. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowObservation_meromorphic line 107
  9. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowObservation_right line 112
  10. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowObservation_residue line 128