OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphBackward.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The convergent backward sum in the graph construction

The inverse unstable evolution only needs operator norm at most one. The factor 2⁻ʲ from the weighted sequence space supplies summability, including the neutral phase coordinate. The bound is exactly the geometric cost two.

  1. theorem OAI.DefocusingNLS.stableBackward_term_bound line 20
  2. theorem OAI.DefocusingNLS.stableBackward_summable line 41
  3. theorem OAI.DefocusingNLS.stableBackward_sum_bound line 49
  4. def OAI.DefocusingNLS.stableBackward line 60

    Source documentation

    Negative backward solution of the normalized unstable recurrence.

    noncomputable def stableBackward (R : E →L[ℝ] E) (hR : ‖R‖ ≤ 1)
    (f : ℕ →ᵇ E) : ℕ →ᵇ E :=
…
  5. theorem OAI.DefocusingNLS.stableBackward_apply line 66
  6. theorem OAI.DefocusingNLS.norm_stableBackward_le line 71
  7. theorem OAI.DefocusingNLS.stableBackward_sub line 77
  8. theorem OAI.DefocusingNLS.stableBackward_dist_le line 86