OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEulerPhysical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Falling Euler derivatives are the actual radial derivatives

This identity converts the exact logarithmic coefficient recurrence back to the top physical derivative occurring in the homogeneous Sobolev norm.

  1. theorem OAI.DefocusingNLS.homogeneousPair_iteratedDeriv_smooth line 19
  2. theorem OAI.DefocusingNLS.homogeneousEulerDeriv_physical line 28