ExpandingBielecki.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The moving-scale mild equation on arbitrary finite slabs

An exponential time weight makes the Picard map contract with constant K / (K + 1) on every finite interval. Thus the permitted slab length is independent of the initial radius and requires no a priori small-time bound.

def OAI.DefocusingNLS.expandingTimeWeight line 19
theorem OAI.DefocusingNLS.expandingTimeWeight_cancel line 25
def OAI.DefocusingNLS.expandingBieleckiHistory line 33
theorem OAI.DefocusingNLS.continuous_expandingBieleckiHistory line 38
def OAI.DefocusingNLS.expandingBieleckiPicard line 44

theorem OAI.DefocusingNLS.expandingBieleckiPicard_dist_le line 52

Source documentation

The weighted Picard bound is independent of both radius and slab length.

theorem expandingBieleckiPicard_dist_le (a b k L T η : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T) (hη : 0 < η)
    (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 (expandingBieleckiPicard a b k L T η ha hk hL hT F u₀ u)
      (expandingBieleckiPicard a b k L T η ha hk hL hT F u₀ v) ≤ K / η * dist u v := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingBieleckiPicard

theorem OAI.DefocusingNLS.existsUnique_expandingMildSolution_finiteSlab line 101

Source documentation

Globally Lipschitz continuous reactions have a unique moving-scale mild solution on every finite slab. In particular, the actual bounded linearized potential does.

theorem existsUnique_expandingMildSolution_finiteSlab (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 : 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