OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphProjectedRecurrence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The projected contraction retains the original endpoint dynamics

Preprojecting the stable block extends its kernel estimate to a bounded operator on the fixed ambient space. The fixed forward sequence remains in the correct kernels, so that extension does not alter its recurrence.

  1. theorem OAI.DefocusingNLS.stableProjected_forward_identity line 17
  2. theorem OAI.DefocusingNLS.stableProjected_reconstruct_recurrence line 25