OAI/NumberTheory/CubicMoment/Theta/CubicThetaWindowEquation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compact incoming window satisfies its exact global differential equation, with the original forcing minus the high annular forcing.

  1. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowTerm_equation line 13
  2. lemma OAI.CubicFirstMoment.window_coordinate_smooth line 36
  3. lemma OAI.CubicFirstMoment.cubicThetaIncomingWindowFinite_equation line 52
  4. theorem OAI.CubicFirstMoment.cubicThetaIncomingWindow_equation line 66