OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEnergyGenerator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite contour generator at a prescribed coercive Sobolev order

  1. theorem OAI.DefocusingNLS.homogeneousLinearized_finite_generator_of_gap line 17