OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedShellBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual odd-power profile supplies all forcing estimates in the coupled shell absorption argument. Only the scalar comparison data and the remote outgoing condition remain at this interface.

  1. theorem OAI.DefocusingNLS.radialMatched_shell_boundary_absorb line 14