OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDuhamelDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The strong initial derivative of the actual Duhamel term

Continuity of the forcing suffices at the initial time. This is the bounded-perturbation part of the generator of the constructed evolution.

  1. theorem OAI.DefocusingNLS.hasDerivAt_zero_smul_continuous line 18
  2. theorem OAI.DefocusingNLS.hasDerivAt_homogeneousDuhamel_zero line 28