OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFreeAnnulus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A genuine subunit annulus for the boundary-normalized free exterior.

  1. theorem OAI.DefocusingNLS.radialFreeSlowValue_tendsto line 11
  2. theorem OAI.DefocusingNLS.radialFreeSlow_annulus line 24
  3. def OAI.DefocusingNLS.radialFreeBoundaryCoefficient line 66
  4. theorem OAI.DefocusingNLS.radialFreeBoundaryCoefficient_spec line 70
  5. theorem OAI.DefocusingNLS.exists_radialExterior_boundary_free_limit line 109