OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPicardContinuity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of the actual moving-scale Picard operator

The reaction is allowed to vary with the parameter in the topology of joint point evaluation. Compactness of the time slab turns this into continuity of its forcing history. Together with the strongly continuous free family and the uniformly bounded Duhamel operator this gives the required path continuity without an operator-norm assertion for Schrödinger evolution.

  1. def OAI.DefocusingNLS.expandingReactionSlab line 21
  2. theorem OAI.DefocusingNLS.continuous_expandingReactionSlab line 26
  3. def OAI.DefocusingNLS.expandingFreeSlab line 37
  4. theorem OAI.DefocusingNLS.continuous_expandingFreeSlab line 47
  5. theorem OAI.DefocusingNLS.expandingPicard_eq_slab line 60
  6. theorem OAI.DefocusingNLS.continuous_expandingPicard_family line 76
  7. theorem OAI.DefocusingNLS.continuous_expandingTimeWeight line 91
  8. theorem OAI.DefocusingNLS.continuous_expandingBieleckiPicard_family line 97