ExpandingResidualStability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Short-slab stability from the actual nonlinear mild defect

The Lipschitz estimate is required only along the two bounded trajectories. No global Lipschitz hypothesis is imposed on the odd-power polynomial.

theorem OAI.DefocusingNLS.exists_expandingOddPower_lipschitz_on_ball line 20
def OAI.DefocusingNLS.expandingNonlinearReaction line 37
theorem OAI.DefocusingNLS.expandingPicard_pair_dist_le line 46
theorem OAI.DefocusingNLS.expandingPicard_initial_dist_le line 77
theorem OAI.DefocusingNLS.expandingMild_residual_stability line 94

theorem OAI.DefocusingNLS.exists_expandingNonlinear_residual_stability line 123

Source documentation

The short-time stability constant for the actual odd-power equation is independent of the starting scale.

theorem exists_expandingNonlinear_residual_stability (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), T * K < 1 →
      ∀ (u v : C(Icc (0 : ℝ) T, FourierL2)),
      (∀ t, ‖u t‖ ≤ R) → (∀ t, ‖v t‖ ≤ R) → ∀ (u₀ v₀ : FourierL2) (ε : ℝ),
      u = expandingPicard a b k L T ha hk hL hT
        (expandingNonlinearReaction a k L T ha ha1 hk hL m) u₀ u →
      dist v (expandingPicard a b k L T ha hk hL hT
        (expandingNonlinearReaction a k L T ha ha1 hk hL m) v₀ v) ≤ ε →
      dist u v ≤ (dist u₀ v₀ + ε) / (1 - T * K) := by
…

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