OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedRadial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The zero angular mode of the actual primary projection, with its constant-to-Fourier ratio retained in the pole coefficient.

  1. lemma OAI.CubicFirstMoment.cubicThetaBoundedScaledAxis_zero line 13
  2. def OAI.CubicFirstMoment.cubicThetaSelectedRadialAxis line 17
  3. def OAI.CubicFirstMoment.cubicThetaProjectedRadialAxis line 21
  4. def OAI.CubicFirstMoment.cubicThetaProjectedRadialConstant line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialAxis_reciprocal line 28
  6. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialAxis_small line 51
  7. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadialAxis_small line 59
  8. def OAI.CubicFirstMoment.cubicThetaSelectedRadialCompleted line 66
  9. def OAI.CubicFirstMoment.cubicThetaProjectedRadialCompleted line 72
  10. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadial_mellin line 78
  11. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadial_mellin line 92
  12. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialCompleted_functional line 106