OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedRadialC2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global C² data retained for the nonzero matched radial channel

The global regularity already follows from angular differentiation of the physical eigenfunction. Keeping it here allows the actual weak-energy bridge to use the origin without assuming endpoint regularity.

  1. theorem OAI.DefocusingNLS.homogeneous_matched_contour_nonzero_radial_c2 line 20