OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedShellGreen.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual matched profile supplies the small coupled Green correction. Only the scalar transfer bounds remain as inputs to the fixed-shell estimate.

  1. theorem OAI.DefocusingNLS.radialMatched_shell_green_small line 13