OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedWeakCoefficients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equality of the actual limiting operator and its density-based weak form.

  1. theorem OAI.DefocusingNLS.radialMatchedLimitWeakOperator_eq line 10
  2. theorem OAI.DefocusingNLS.radialMatchedWeak_equation line 28