OAI/NumberTheory/CubicMoment/Theta/CubicThetaWindowProfile.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The exact radial defect of the compact incoming window. Its difference from the original forcing is a continuous weight supported in [2,4].

  1. def OAI.CubicFirstMoment.cubicThetaWindowHeight line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaWindowHeight_smooth line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaWindowHeight_zero line 27
  4. def OAI.CubicFirstMoment.cubicThetaWindowDefect line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaWindowDefect_continuous line 37
  6. lemma OAI.CubicFirstMoment.cubicThetaWindowDefect_zero_open line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaWindowDefect_low line 58
  8. lemma OAI.CubicFirstMoment.cubicThetaIncomingForcing_continuous line 77
  9. def OAI.CubicFirstMoment.cubicThetaHighWindowForcing line 87
  10. lemma OAI.CubicFirstMoment.cubicThetaHighWindowForcing_continuous line 90
  11. lemma OAI.CubicFirstMoment.cubicThetaHighWindowForcing_low line 94
  12. lemma OAI.CubicFirstMoment.cubicThetaHighWindowForcing_high line 102
  13. def OAI.CubicFirstMoment.cubicThetaHighWindowWeight line 112
  14. lemma OAI.CubicFirstMoment.cubicThetaWindowHeight_equation line 124