OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphSplitSource.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Splitting a nonlinear endpoint remainder into graph coordinates

These operator estimates implement the two source terms in the forward and backward graph equations. The unstable coordinate is weighted by K; the small linear defect and nonlinear remainder remain explicit quantities.

  1. theorem OAI.DefocusingNLS.stableGraph_split_source_lipschitz line 17
  2. theorem OAI.DefocusingNLS.stableGraph_split_source_zero line 73