OAI/NumberTheory/CubicMoment/Theta/CubicThetaLongWindowKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual theta kernel can be paired with the incoming forcing in an arbitrarily high compact annulus.

  1. lemma OAI.CubicFirstMoment.cubicThetaIncomingForcingWeight_low line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaLongForcingWeight_low_one line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaLongForcingWeight_low_two line 23
  4. def OAI.CubicFirstMoment.cubicThetaLongWindowTest line 27
  5. def OAI.CubicFirstMoment.cubicThetaLongWindowDefect line 32
  6. lemma OAI.CubicFirstMoment.cubicThetaLongWindowDefect_low line 35
  7. def OAI.CubicFirstMoment.cubicThetaLongWindowDefectSection line 40
  8. lemma OAI.CubicFirstMoment.cubicThetaLongWindowDefectSection_compact line 44
  9. lemma OAI.CubicFirstMoment.cubicThetaLongWindowDefectSection_eq line 48
  10. lemma OAI.CubicFirstMoment.cubicThetaLongWindowDefectL2 line 55
  11. lemma OAI.CubicFirstMoment.cubicThetaLongWindow_coordinate_equation line 72
  12. lemma OAI.CubicFirstMoment.cubicThetaLongWindow_global_weak line 85
  13. lemma OAI.CubicFirstMoment.cubicThetaKernel_long_window_balance line 97
  14. theorem OAI.CubicFirstMoment.cubicThetaResidue_long_kernel_pairing line 121