OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExponentialInterpolation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a rapidly decaying remainder using only a coarse second derivative.

  1. theorem OAI.DefocusingNLS.radial_derivative_exp_interpolation line 11