OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialLogarithmicSymbol.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Symbol estimates in logarithmic radius before composition with the radial coordinate.

  1. theorem OAI.DefocusingNLS.radial_complexExp_contDiff line 12
  2. theorem OAI.DefocusingNLS.radial_complexExp_iteratedDeriv line 16
  3. theorem OAI.DefocusingNLS.radial_logarithmic_product_bound line 30
  4. theorem OAI.DefocusingNLS.radialExteriorCanonical_logarithmic_symbol line 64