OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialCartesianSymbol.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cartesian symbol estimates obtained from the actual outgoing expansion.

  1. theorem OAI.DefocusingNLS.radial_log_composition_symbol line 15