OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousWeakNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The norm bound retained by a weak homogeneous limit

  1. theorem OAI.DefocusingNLS.homogeneousY_norm_le_of_weak_limit line 11