OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialPolynomialSubunitLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform disappearance of the polynomial odd power near a subunit constant term.

  1. theorem OAI.DefocusingNLS.radialPolynomial_eventually_subunit_circle line 10
  2. theorem OAI.DefocusingNLS.radialPolynomialPower_uniform_limit line 30