OAI/NumberTheory/CubicMoment/Theta/CubicThetaIncomingWindow.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The difference of incoming cutoffs at heights one and two is a literal compact smooth automorphic section.

  1. def OAI.CubicFirstMoment.cubicThetaIncomingWindowCutoff line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowCutoff_smooth line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowCutoff_low line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowCutoff_high line 27
  5. def OAI.CubicFirstMoment.cubicThetaIncomingWindowTerm line 32
  6. def OAI.CubicFirstMoment.cubicThetaIncomingWindow line 35
  7. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowTerm_translate line 38
  8. theorem OAI.CubicFirstMoment.cubicThetaIncomingWindow_automorphy line 46
  9. theorem OAI.CubicFirstMoment.cubicThetaIncomingWindow_compact_sum line 57
  10. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowTerm_contDiffAt line 68
  11. theorem OAI.CubicFirstMoment.cubicThetaIncomingWindow_contDiffOn line 76
  12. theorem OAI.CubicFirstMoment.cubicThetaIncomingWindow_core line 89
  13. def OAI.CubicFirstMoment.cubicThetaIncomingWindowSection line 109
  14. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowSection_compact line 119
  15. def OAI.CubicFirstMoment.cubicThetaIncomingWindowTest line 130