ExpandingMildContraction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A short-time mild contraction on expanding tori

A jointly continuous reaction with a uniform Lipschitz bound gives a unique mild trajectory whenever T K < 1. The interval length depends on the reaction bound and is independent of the starting torus scale.

def OAI.DefocusingNLS.expandingReactionHistory line 20
theorem OAI.DefocusingNLS.continuous_expandingReactionHistory line 25
def OAI.DefocusingNLS.expandingPicard line 31

theorem OAI.DefocusingNLS.expandingPicard_dist_le line 46

Source documentation

The Picard contraction constant is T K, with no dependence on L.

theorem expandingPicard_dist_le (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (F : C((Icc (0 : ℝ) T) × FourierL2, FourierL2)) (u₀ : FourierL2)
    (K : ℝ) (hK : 0 ≤ K)
    (hF : ∀ t x y, ‖F (t, x) - F (t, y)‖ ≤ K * ‖x - y‖)
    (u v : C(Icc (0 : ℝ) T, FourierL2)) :
    dist (expandingPicard a b k L T ha hk hL hT F u₀ u)
      (expandingPicard a b k L T ha hk hL hT F u₀ v) ≤ T * K * dist u v := by
…

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

theorem OAI.DefocusingNLS.existsUnique_expandingMildSolution line 82

Source documentation

Existence and uniqueness of the actual moving-scale mild equation on a short slab.

theorem existsUnique_expandingMildSolution (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (F : C((Icc (0 : ℝ) T) × FourierL2, FourierL2)) (u₀ : FourierL2)
    (K : ℝ) (hK : 0 ≤ K) (hTK : T * K < 1)
    (hF : ∀ t x y, ‖F (t, x) - F (t, y)‖ ≤ K * ‖x - y‖) :
    ∃! u : C(Icc (0 : ℝ) T, FourierL2), ∀ t : Icc (0 : ℝ) T,
      u t = expandingFreeStep a b k L t ha hk hL t.2.1 u₀ +
        expandingDuhamel a b k L ha hk hL t (expandingReactionHistory T hT F u) := by
…

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

theorem OAI.DefocusingNLS.expandingMildSolution_initialData_bound line 105

Source documentation

Short-slab dependence on the initial datum is uniform in the torus scale.

theorem expandingMildSolution_initialData_bound (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (F : C((Icc (0 : ℝ) T) × FourierL2, FourierL2))
    (u₀ v₀ : FourierL2) (K : ℝ) (hK : 0 ≤ K) (hTK : T * K < 1)
    (hF : ∀ t x y, ‖F (t, x) - F (t, y)‖ ≤ K * ‖x - y‖)
    (u v : C(Icc (0 : ℝ) T, FourierL2))
    (hu : ∀ t : Icc (0 : ℝ) T, u t =
      expandingFreeStep a b k L t ha hk hL t.2.1 u₀ +
        expandingDuhamel a b k L ha hk hL t (expandingReactionHistory T hT F u))
    (hv : ∀ t : Icc (0 : ℝ) T, v 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 F v)) :
…

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

def OAI.DefocusingNLS.expandingLinearReaction line 146

Source documentation

The real-linear potential enters with the exact Schrödinger factor -i.

noncomputable def expandingLinearReaction (T : ℝ)
    (B : C(Icc (0 : ℝ) T, FourierL2 →L[ℝ] FourierL2))
    (g : C(Icc (0 : ℝ) T, FourierL2)) :
    C((Icc (0 : ℝ) T) × FourierL2, FourierL2) where
…

Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.expandingLinearReaction_lipschitz line 155

theorem OAI.DefocusingNLS.existsUnique_expandingLinearMildSolution line 169

Source documentation

Uniformly bounded continuous real-linear potentials have a unique short-slab propagator, including a continuous source term.

theorem existsUnique_expandingLinearMildSolution (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (B : C(Icc (0 : ℝ) T, FourierL2 →L[ℝ] FourierL2))
    (g : C(Icc (0 : ℝ) T, FourierL2)) (u₀ : FourierL2)
    (K : ℝ) (hK : 0 ≤ K) (hTK : T * K < 1) (hB : ∀ t, ‖B t‖ ≤ K) :
    ∃! u : C(Icc (0 : ℝ) T, FourierL2), ∀ t : Icc (0 : ℝ) T,
      u t = expandingFreeStep a b k L t ha hk hL t.2.1 u₀ +
        expandingDuhamel a b k L ha hk hL t
          (expandingReactionHistory T hT (expandingLinearReaction T B g) u) :=
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingReactionHistory, OAI.DefocusingNLS.expandingLinearReaction