OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedRadialMellin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Entire radial factors for the actual shifted frequency, including a finite closed height window. The endpoint changes are null sets.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedPositiveRadialTest line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedRadial_height_dilation line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaShiftedPositiveRadial_integrable line 41
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedPositiveRadial_mellin line 52
  5. lemma OAI.CubicFirstMoment.cubicThetaShiftedPositiveRadial_entire line 78
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowRadial_sub line 88
  7. lemma OAI.CubicFirstMoment.cubicThetaShiftedWindowRadial_entire line 97