OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphReconstruction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing the actual endpoint recurrence from graph coordinates

The frame and coordinate maps are explicit operators. Their identities ensure the projected stable recurrence stays in the correct kernel and the two graph recurrences combine into the original nonlinear endpoint step. No spectral estimates are assumed by this algebraic supporting lemma.

  1. def OAI.DefocusingNLS.stableFrameProjection line 21
  2. theorem OAI.DefocusingNLS.stableFrameProjection_coordinate line 24
  3. theorem OAI.DefocusingNLS.stableFrameProjection_decomposition line 29
  4. def OAI.DefocusingNLS.stableFrameState line 32
  5. theorem OAI.DefocusingNLS.stableFrameState_coordinate line 35
  6. theorem OAI.DefocusingNLS.stableFrame_forward_split line 40
  7. theorem OAI.DefocusingNLS.stableFrame_forward_kernel line 47
  8. theorem OAI.DefocusingNLS.stableGraph_reconstruct_recurrence line 59
  9. theorem OAI.DefocusingNLS.stableFrameState_norm_le line 85
  10. theorem OAI.DefocusingNLS.stableFrameState_weighted_norm_le line 91
  11. theorem OAI.DefocusingNLS.stableFrameState_weighted_tendsto_zero line 103