OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPositivePower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for positive powers in the expanding Sobolev algebra

  1. theorem OAI.DefocusingNLS.expandingProduct_one_right line 10
  2. theorem OAI.DefocusingNLS.expandingPower_one line 18
  3. theorem OAI.DefocusingNLS.expandingPower_positive_norm_le line 25
  4. theorem OAI.DefocusingNLS.expandingAnticircularCoefficient_one line 43