OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSymbolProducts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Product estimates for the two polynomial coefficients of the actual linearized potential.

  1. def OAI.DefocusingNLS.HasCartesianSymbol line 14
  2. theorem OAI.DefocusingNLS.HasCartesianSymbol.const line 18
  3. theorem OAI.DefocusingNLS.HasCartesianSymbol.mul line 28
  4. theorem OAI.DefocusingNLS.HasCartesianSymbol.conj line 66
  5. theorem OAI.DefocusingNLS.HasCartesianSymbol.const_mul line 76
  6. theorem OAI.DefocusingNLS.HasCartesianSymbol.pow line 80
  7. theorem OAI.DefocusingNLS.radialMatchedCartesian_hasCartesianSymbol line 89