OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExteriorBoundedFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Common real-tail extensions of the uniformly convergent polynomial families.

  1. def OAI.DefocusingNLS.radialExteriorTailVariable line 12
  2. theorem OAI.DefocusingNLS.radialExteriorTailVariable_mem line 14
  3. def OAI.DefocusingNLS.boundedRadialPolynomialAfter line 19
  4. theorem OAI.DefocusingNLS.boundedRadialPolynomialAfter_apply line 29
  5. theorem OAI.DefocusingNLS.boundedRadialPolynomialAfter_eq line 32
  6. theorem OAI.DefocusingNLS.boundedRadialPolynomialAfter_limit line 37
  7. def OAI.DefocusingNLS.boundedRadialResidualAfter line 60
  8. theorem OAI.DefocusingNLS.boundedRadialResidualAfter_apply line 68
  9. theorem OAI.DefocusingNLS.boundedRadialResidualAfter_difference line 71
  10. theorem OAI.DefocusingNLS.boundedRadialResidualAfter_limit line 82
  11. theorem OAI.DefocusingNLS.boundedRadialResidualAfter_factor line 93
  12. theorem OAI.DefocusingNLS.exists_radialExterior_bounded_residual_family line 109