OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphWeightedSource.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Endpoint remainders define bounded weighted sequence sources

The zero-data remainder decays geometrically along the expanding radii. Pointwise Lipschitz bounds on a small state ball therefore give a bounded Lipschitz map on the weighted sequence ball. The extension outside that ball is used only to supply a total function to the local contraction.

  1. theorem OAI.DefocusingNLS.stableSequenceValue_norm_le line 20
  2. def OAI.DefocusingNLS.stableWeightedSourceTerm line 27
  3. theorem OAI.DefocusingNLS.stableWeightedSourceTerm_bound line 30
  4. theorem OAI.DefocusingNLS.stableWeightedSourceTerm_dist_le line 60
  5. def OAI.DefocusingNLS.stableWeightedSource line 85
  6. theorem OAI.DefocusingNLS.stableWeightedSource_norm_le line 95
  7. theorem OAI.DefocusingNLS.stableWeightedSource_dist_le line 107
  8. def OAI.DefocusingNLS.stablePairSequence line 126

    Source documentation

    Package the stable and unstable weighted coordinates into one sequence.

    noncomputable def stablePairSequence (x : (ℕ →ᵇ E) × (ℕ →ᵇ F)) : ℕ →ᵇ E × F :=
…
  9. theorem OAI.DefocusingNLS.norm_stablePairSequence_le line 133
  10. theorem OAI.DefocusingNLS.stablePairSequence_dist_le line 141