OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexVirial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact complex scalar virial formula is the sum of the two checked real formulas, with the physical outer boundary retained.

  1. def OAI.DefocusingNLS.radialComplexAngularForm line 12
  2. def OAI.DefocusingNLS.radialComplexAngularVirial line 17
  3. def OAI.DefocusingNLS.radialComplexAngularBoundary line 22
  4. theorem OAI.DefocusingNLS.radialComplexAngular_virial_identity line 27