OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLocalizationContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the actual radius-dependent localization

Localization at radius L factors through the fixed radius-one localization, the exact inverse weight transfer, and physical homogeneous dilation.

  1. theorem OAI.DefocusingNLS.homogeneousLocalization_dilation line 24
  2. theorem OAI.DefocusingNLS.continuous_homogeneousLocalization line 49
  3. theorem OAI.DefocusingNLS.continuous_expandingCoordinates_apply line 70