OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphSequence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The weighted sequence space for the nonlinear stable graph

A bounded sequence records 2^n times the physical perturbation. Thus the ambient sequence space is Banach without imposing an auxiliary completeness assumption on decaying sequences. These are supporting lemmas for nl:graph; no spectral splitting or nonlinear evolution is assumed here.

  1. def OAI.DefocusingNLS.stableSequenceValue line 27

    Source documentation

    The actual value of a perturbation encoded in the weighted sequence space.

    noncomputable def stableSequenceValue (x : ℕ →ᵇ E) (n : ℕ) : E :=
…
  2. theorem OAI.DefocusingNLS.norm_stableSequenceValue_le line 30
  3. theorem OAI.DefocusingNLS.stableSequenceValue_tendsto_zero line 36
  4. theorem OAI.DefocusingNLS.stableSequenceValue_zero line 42
  5. theorem OAI.DefocusingNLS.stableSequenceValue_succ line 45
  6. theorem OAI.DefocusingNLS.stableSequence_geometric_source_bound line 49