OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedBoundedPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded C² data for the nonzero matched radial channel

The faithful physical realization is a C₀ function. The same spherical test used to obtain a nonzero channel therefore gives a global uniform bound, alongside the exact radial equation and top-derivative square integrability.

  1. theorem OAI.DefocusingNLS.homogeneous_matched_contour_nonzero_bounded_radial line 21