OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffResidualJets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite jets of the normalized cutoff residual

  1. theorem OAI.DefocusingNLS.normalizedPhysicalProfile_fderiv line 13
  2. theorem OAI.DefocusingNLS.weightedJet_add line 28
  3. theorem OAI.DefocusingNLS.weightedJet_sum line 39
  4. theorem OAI.DefocusingNLS.weightedJet_two_smul line 50
  5. theorem OAI.DefocusingNLS.weightedJet_assembly line 60
  6. theorem OAI.DefocusingNLS.gradient_compact line 86
  7. theorem OAI.DefocusingNLS.laplacian_compact line 91
  8. theorem OAI.DefocusingNLS.power_compact line 96
  9. def OAI.DefocusingNLS.normalizedCutoffResidualSchwartz line 100
  10. theorem OAI.DefocusingNLS.normalizedCutoffResidualSchwartz_apply line 115
  11. theorem OAI.DefocusingNLS.exists_normalizedCutoffResidual_uniform_jets line 128