OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphSourceIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact values of the weighted graph sources

The bounded extension used outside the sequence ball has no effect on its fixed point. Removing the geometric weight recovers the actual pointwise nonlinear source on that ball.

  1. theorem OAI.DefocusingNLS.stableWeightedSource_value line 19
  2. theorem OAI.DefocusingNLS.stablePairSequence_value line 35
  3. def OAI.DefocusingNLS.stableFrameAssembly line 39
  4. theorem OAI.DefocusingNLS.stableFrameAssembly_apply line 42
  5. theorem OAI.DefocusingNLS.stableFrameAssembly_norm_le line 45