OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzScaledCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite jets after a slowly varying cutoff

On normalized annuli the extra cutoff is χ(δ x), with 0 < δ ≤ 1. Its derivatives cost no inverse scale, so the same finite jet bound is uniform in δ.

  1. def OAI.DefocusingNLS.schwartzScaledCutoff line 17
  2. theorem OAI.DefocusingNLS.schwartzScaledCutoff_apply line 22
  3. def OAI.DefocusingNLS.schwartzCutoffJetConstant line 26
  4. theorem OAI.DefocusingNLS.schwartzCutoffJetConstant_nonneg line 30
  5. theorem OAI.DefocusingNLS.schwartzScaledCutoff_jet_bound line 35