OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedPencilExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nonzero free matching determinant excludes nearby matched weak kernels. The weights and pressure may be supplied by radialMatched_penaltyFamily.

  1. theorem OAI.DefocusingNLS.radialMatchedPencil_eventually_kernel_zero line 14