OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphFrameBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded frame normalization for the concrete torus blocks

The stable estimate in the manuscript is only on the coordinate kernel. Precomposing with the bounded stable projection gives the whole-space block used by the sequence contraction. Scaling the finite-dimensional frame makes the mixed block small without changing that projection.

  1. def OAI.DefocusingNLS.stableNormalizedFrame line 18
  2. def OAI.DefocusingNLS.stableNormalizedCoordinate line 21
  3. theorem OAI.DefocusingNLS.stableNormalized_rightInverse line 24
  4. theorem OAI.DefocusingNLS.stableNormalized_projection line 30
  5. theorem OAI.DefocusingNLS.stableNormalizedFrame_norm_le line 40
  6. theorem OAI.DefocusingNLS.stableNormalizedCoordinate_norm_le line 46
  7. theorem OAI.DefocusingNLS.stableNormalized_defect line 51
  8. theorem OAI.DefocusingNLS.stableNormalized_defect_norm_le line 60
  9. def OAI.DefocusingNLS.stableProjectedBlock line 68
  10. def OAI.DefocusingNLS.stableMixedBlock line 72
  11. theorem OAI.DefocusingNLS.stableFrameProjection_eq_self line 76
  12. theorem OAI.DefocusingNLS.stableProjectedBlock_norm_le line 81
  13. theorem OAI.DefocusingNLS.stableProjectedBlock_norm_le_eighth line 97
  14. theorem OAI.DefocusingNLS.stableMixedBlock_norm_le line 108
  15. theorem OAI.DefocusingNLS.stableNormalized_mixed_norm_le line 125