OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialInnerFixedPoint.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A genuine fixed point of the coupled inner amplitude equation.

  1. structure OAI.DefocusingNLS.RadialInnerData line 13

    Source documentation

    Only numerical parameter conditions; no analytic conclusion is part of the data.

    structure RadialInnerData where
…
  2. theorem OAI.DefocusingNLS.RadialInnerData.lo_lower line 32
  3. def OAI.DefocusingNLS.radialInnerClampedInput line 35
  4. theorem OAI.DefocusingNLS.radialInnerClampedInput_continuous line 38
  5. theorem OAI.DefocusingNLS.radialInnerClampedInput_mem line 42
  6. def OAI.DefocusingNLS.radialInnerRaw line 46
  7. theorem OAI.DefocusingNLS.radialInnerRaw_spec line 52
  8. def OAI.DefocusingNLS.radialInnerOperator line 59
  9. theorem OAI.DefocusingNLS.radialInnerOperator_contracting line 69
  10. theorem OAI.DefocusingNLS.exists_radial_coupled_profile line 96