OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFreeShootingData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A continuous boundary jet of the actual free inner IVP on the certified disk.

  1. abbrev OAI.DefocusingNLS.RadialShootingDisk line 12
  2. def OAI.DefocusingNLS.radialShootingB line 14
  3. def OAI.DefocusingNLS.radialShootingZ line 17
  4. def OAI.DefocusingNLS.radialShootingR line 20
  5. theorem OAI.DefocusingNLS.radialShooting_geometry line 23
  6. theorem OAI.DefocusingNLS.exists_radialFreeInnerJet line 45
  7. def OAI.DefocusingNLS.radialFreeInnerJet line 64
  8. theorem OAI.DefocusingNLS.radialFreeInnerJet_spec line 67
  9. theorem OAI.DefocusingNLS.continuous_radialFreeInner_boundary line 80