OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialTruncatedNonlinearity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The bounded polynomial truncation used in the positive radial Dirichlet problem.

  1. def OAI.DefocusingNLS.radialAmplitudeClamp line 11
  2. theorem OAI.DefocusingNLS.radialAmplitudeClamp_mem line 13
  3. theorem OAI.DefocusingNLS.radialAmplitudeClamp_eq line 17
  4. theorem OAI.DefocusingNLS.radialAmplitudeClamp_lipschitz line 21
  5. theorem OAI.DefocusingNLS.unit_interval_power_difference line 25
  6. def OAI.DefocusingNLS.radialTruncatedNonlinearity line 38
  7. theorem OAI.DefocusingNLS.continuous_radialTruncatedNonlinearity line 42
  8. theorem OAI.DefocusingNLS.radialTruncatedNonlinearity_bound line 48
  9. theorem OAI.DefocusingNLS.radialTruncatedNonlinearity_lipschitz line 66