ExpandingFiniteSlab.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-slab bounds for the actual moving potential

The Bielecki construction applies on every finite interval. Its initial-data bound depends only on the slab length and the uniform bound on the profile, not on the initial radius of the expanding torus.

theorem OAI.DefocusingNLS.expandingTimeWeight_dist_le line 19

theorem OAI.DefocusingNLS.expandingBielecki_isFixedPt line 35

Source documentation

Every mild trajectory becomes a fixed point of the weighted Picard map.

theorem expandingBielecki_isFixedPt (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)
    (u : 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)) :
    Function.IsFixedPt (expandingBieleckiPicard a b k L T η ha hk hL hT F u₀)
      (expandingTimeWeight T (-η) u) := by
…

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

theorem OAI.DefocusingNLS.expandingMildSolution_finiteSlab_initialData_bound line 55

Source documentation

Dependence on the initial datum, uniformly in L, on an arbitrary finite slab.

theorem expandingMildSolution_finiteSlab_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)
    (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

theorem OAI.DefocusingNLS.existsUnique_expandingProfile_finiteSlab line 120

Source documentation

The actual odd-power linearization along a bounded profile has a unique solution on every finite slab, at every permitted starting radius.

theorem existsUnique_expandingProfile_finiteSlab (a b k L T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (m : ℕ) (R : ℝ) (hR : 0 ≤ R)
    (q g : C(Icc (0 : ℝ) T, FourierL2)) (u₀ : FourierL2) (hq : ∀ t, ‖q t‖ ≤ R) :
    ∃! 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
            (expandingProfileReaction a k T ha ha1 hk m (expandingRadiusCurve L T hL) q g) u) := by
…

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