OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousGluedOriginRegularity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integer angular modes have all regular-origin derivatives; no expansion is assumed.

  1. theorem OAI.DefocusingNLS.homogeneousGlued_origin_regularity line 13