OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingDuhamelFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Joint scale and forcing continuity of the finite-slab Duhamel operator

The operator has a uniform finite-slab bound and is strongly continuous in the starting radius. These two properties give joint continuity in the radius and the forcing path, without operator-norm continuity of the free Schrödinger propagator.

  1. theorem OAI.DefocusingNLS.continuous_operator_apply_of_uniform_bound line 19
  2. def OAI.DefocusingNLS.expandingForcingExtension line 39
  3. theorem OAI.DefocusingNLS.continuous_expandingForcingExtension line 43
  4. def OAI.DefocusingNLS.expandingDuhamelSlab line 47
  5. theorem OAI.DefocusingNLS.expandingDuhamelSlab_apply line 83
  6. theorem OAI.DefocusingNLS.expandingDuhamelSlab_norm_le line 89
  7. theorem OAI.DefocusingNLS.continuous_expandingDuhamelSlab_strong line 102
  8. theorem OAI.DefocusingNLS.continuous_expandingDuhamelSlab line 114