ExpandingPerturbationExistence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small nonlinear perturbations on an arbitrary fixed step

The nonlinear reaction is the actual odd-power increment around a bounded profile. Its local Lipschitz constant and its admissible forcing size are uniform in the starting torus radius.

theorem OAI.DefocusingNLS.exists_expandingPerturbationReaction_local_lipschitz line 18
theorem OAI.DefocusingNLS.expandingPerturbationReaction_zero line 37

theorem OAI.DefocusingNLS.exists_expandingPerturbation_finiteSlab line 46

Source documentation

The step length may be fixed arbitrarily. Smallness depends on that length and the fixed profile bound, not on the starting torus radius.

theorem exists_expandingPerturbation_finiteSlab (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (hT : 0 ≤ T)
      (q g : C(Icc (0 : ℝ) T, FourierL2)) (v₀ : FourierL2) (G : ℝ),
      0 ≤ G → (∀ t, ‖q t‖ ≤ R) → (∀ t, ‖g t‖ ≤ G) →
      (K + 1) * ‖v₀‖ + G ≤ Real.exp (-(K + 1) * T) →
      ∃ v : C(Icc (0 : ℝ) T, FourierL2),
        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 ∧
        ‖v‖ ≤ Real.exp ((K + 1) * T) * ((K + 1) * ‖v₀‖ + G) ∧ ‖v‖ ≤ 1 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingPicard, OAI.DefocusingNLS.expandingPerturbationReaction