OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialProfileDerivativeBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radial top-derivative bounds for the actual smooth profile, obtained by restricting its already proved Cartesian symbol estimates to a unit ray.

  1. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_derivative_bound line 16
  2. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_top_integrable line 44
  3. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_bounded line 86