ExpandingNonlinearStepError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quadratic deviation from the actual linearized evolution

On a fixed finite slab, a bounded nonlinear perturbation differs from its linearized evolution by the quadratic Taylor term and the profile defect. This is the quantitative comparison part of the manuscript's nl:step.

theorem OAI.DefocusingNLS.expandingPerturbation_linear_mild line 18

theorem OAI.DefocusingNLS.exists_expandingNonlinearStep_quadratic_error line 47

Source documentation

The comparison constant is independent of the starting radius. The perturbation is an actual nonlinear mild solution, not an abstract error.

theorem exists_expandingNonlinearStep_quadratic_error (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ K C : ℝ, 0 ≤ K ∧ 0 ≤ C ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (hT : 0 ≤ T)
      (q g v w : C(Icc (0 : ℝ) T, FourierL2)) (v₀ : FourierL2) (d G : ℝ),
      0 ≤ d → d ≤ 1 → 0 ≤ G → (∀ t, ‖q t‖ ≤ R) → (∀ t, ‖g t‖ ≤ G) →
      (∀ t, ‖v t‖ ≤ d) →
      v = expandingPicard a b k L T ha hk hL hT
        (expandingPerturbationReaction a k L T ha ha1 hk hL m q g) v₀ v →
      (∀ t : Icc (0 : ℝ) T, w t =
        expandingFreeStep a b k L t ha hk hL t.2.1 v₀ +
          expandingDuhamel a b k L ha hk hL t
            (expandingReactionHistory T hT
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingPicard, OAI.DefocusingNLS.expandingPerturbationReaction, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingReactionHistory