OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialPhysicalPencilLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact-pencil lifts retaining the actual physical radial functions

  1. structure OAI.DefocusingNLS.SpectralPhysicalGaugeLift line 15
  2. theorem OAI.DefocusingNLS.SpectralPhysicalGaugeLift.observation_ne_zero line 29
  3. theorem OAI.DefocusingNLS.SpectralPhysicalGaugeLift.physical_eq_of_observation line 47
  4. theorem OAI.DefocusingNLS.radialMatchedPhysical_pencil_lift line 81