OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffFiniteJets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite derivative bounds used by the cutoff residual

The nonlinear estimate concerns the actual scalar odd-power polynomial. The annular estimate only uses derivatives where the compact coefficient lives.

  1. theorem OAI.DefocusingNLS.exists_oddPower_finiteJet_bound line 18
  2. def OAI.DefocusingNLS.annularCoefficientProduct line 62
  3. theorem OAI.DefocusingNLS.annularCoefficientProduct_apply line 66
  4. theorem OAI.DefocusingNLS.annularCoefficientProduct_jet_bound line 70
  5. theorem OAI.DefocusingNLS.norm_iteratedFDeriv_directional_le line 112