OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedRadial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Radial channels of the actual matched-profile contour generator

The profile is the already constructed matched stationary solution. Its smoothness supplies the exterior hypothesis of the radial L² theorem.

  1. theorem OAI.DefocusingNLS.homogeneous_matched_contour_radial line 21