OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphParameterSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous parameter selection for the contracting stable graph

Only strong continuity of the linear blocks and coordinate continuity of the sources are used. The backward inverse is fixed while the starting radius and initial data vary.

  1. theorem OAI.DefocusingNLS.stableGraph_source_norm_le line 24
  2. theorem OAI.DefocusingNLS.exists_continuous_stableGraph_selection line 35