OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousGluedOrigin.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smoothness through the origin for the actual regular Volterra solutions.

  1. theorem OAI.DefocusingNLS.homogeneousGlued_average_congr line 13
  2. theorem OAI.DefocusingNLS.homogeneousGlued_regular_origin line 24
  3. theorem OAI.DefocusingNLS.homogeneousGlued_regular_physical_origin line 66