OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffLinearizedPropagator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-slab evolution for the actual cutoff profile

The matched profile's proved symbol bounds give a single norm bound on all of its expanding-torus samples. The actual linearized potential then has bounded real-linear propagators uniformly in the starting radius.

  1. theorem OAI.DefocusingNLS.exists_matchedCutoffProfile_uniform_bound line 22
  2. theorem OAI.DefocusingNLS.exists_matchedCutoffLinearized_propagator line 40