OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexVirialCoercivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual pressure and deformation estimates give uniform complex virial coercivity, with only the first-component L2 mass as an error.

  1. theorem OAI.DefocusingNLS.radialComplexShiftedVirial_coercive line 15
  2. theorem OAI.DefocusingNLS.radialMatched_complex_virial_coercive line 50