OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSlabMild.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

From adjacent mild equations to the global similarity equation

The exact restart identity transports the actual forcing at each successive radius. Consequently a continuous path satisfying the equation on every equal slab satisfies the original mild equation on every finite interval.

  1. theorem OAI.DefocusingNLS.expandingPicard_initial line 20
  2. theorem OAI.DefocusingNLS.expandingDuhamel_congr_on line 30
  3. theorem OAI.DefocusingNLS.expandingMild_global_of_local line 40
  4. def OAI.DefocusingNLS.expandingGlobalReaction line 84
  5. theorem OAI.DefocusingNLS.continuousOn_expandingGlobalReaction line 90
  6. theorem OAI.DefocusingNLS.expandingGlobalReaction_history line 104
  7. theorem OAI.DefocusingNLS.expandingGlobal_picard_of_local line 118