ExpandingApproximateExistence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact trajectories in a neighborhood of an approximate mild solution

The contraction is restricted to a closed ball of paths, so only the actual local Lipschitz estimate for the polynomial reaction is used.

theorem OAI.DefocusingNLS.expandingMildSolution_initial line 17
theorem OAI.DefocusingNLS.expandingMild_neighborhood_unique line 26
theorem OAI.DefocusingNLS.exists_expandingMild_near_approximation line 38

theorem OAI.DefocusingNLS.exists_expandingNonlinear_near_approximation line 78

Source documentation

The local existence radius and Lipschitz constant are independent of the starting torus scale. The reaction is the actual odd-power nonlinearity.

theorem exists_expandingNonlinear_near_approximation (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (R ρ : ℝ) (hR : 0 ≤ R) (hρ : 0 ≤ ρ) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (hT : 0 ≤ T), T * K < 1 →
      ∀ (v : C(Icc (0 : ℝ) T, FourierL2)), (∀ t, ‖v t‖ ≤ R) →
      ∀ (u₀ : FourierL2) (ε : ℝ),
      dist v (expandingPicard a b k L T ha hk hL hT
        (expandingNonlinearReaction a k L T ha ha1 hk hL m) u₀ v) ≤ ε →
      ε ≤ (1 - T * K) * ρ →
      ∃ u : C(Icc (0 : ℝ) T, FourierL2),
        u = expandingPicard a b k L T ha hk hL hT
          (expandingNonlinearReaction a k L T ha ha1 hk hL m) u₀ u ∧
…

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