OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/NormalizedFrameLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A normalized right inverse bounds its coordinate normalization from below

  1. theorem OAI.DefocusingNLS.normalized_coordinate_lower_bound line 11
  2. theorem OAI.DefocusingNLS.normalized_stable_projection_bound line 25