ExpandingPotentialContinuity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual nonautonomous linearized potential

A continuous profile and a continuous expanding radius give the potential -i D(|u|^(2m)u)|q(t). Its short-time construction uses the uniform exact Y_L derivative bounds already proved, not a separately assumed potential.

def OAI.DefocusingNLS.expandingProfileReaction line 17

Source documentation

The actual real-linearized odd-power reaction along a moving profile.

noncomputable def expandingProfileReaction (a k T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (l : C(Set.Icc (0 : ℝ) T, {L : ℝ // 1 ≤ L}))
    (q g : C(Set.Icc (0 : ℝ) T, FourierL2)) :
    C((Set.Icc (0 : ℝ) T) × FourierL2, FourierL2) where
…

Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.exists_expandingProfileReaction_lipschitz line 33

Source documentation

One Lipschitz bound applies to every starting scale and every bounded profile.

theorem exists_expandingProfileReaction_lipschitz (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (T : ℝ)
      (l : C(Set.Icc (0 : ℝ) T, {L : ℝ // 1 ≤ L}))
      (q g : C(Set.Icc (0 : ℝ) T, FourierL2)),
      (∀ t, ‖q t‖ ≤ R) → ∀ t x y,
      ‖expandingProfileReaction a k T ha ha1 hk m l q g (t, x) -
        expandingProfileReaction a k T ha ha1 hk m l q g (t, y)‖ ≤ K * ‖x - y‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingProfileReaction

def OAI.DefocusingNLS.expandingRadiusCurve line 57
Source documentation
The radius follows exactly the manuscript's moving family L exp(t/2).
```
noncomputable def expandingRadiusCurve (L T : ℝ) (hL : 1 ≤ L) :
    C(Set.Icc (0 : ℝ) T, {M : ℝ // 1 ≤ M}) where
…
```

theorem OAI.DefocusingNLS.expandingProfileReaction_pointwise line 65

Source documentation

The reaction is exactly the scalar linearized Schrödinger potential at each point.

theorem expandingProfileReaction_pointwise (a k T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ)
    (l : C(Set.Icc (0 : ℝ) T, {L : ℝ // 1 ≤ L}))
    (q g : C(Set.Icc (0 : ℝ) T, FourierL2))
    (t : Set.Icc (0 : ℝ) T) (v : FourierL2) (x : SchrodingerTorus) :
    expandingTorusFunction a k (l t).1
      (expandingProfileReaction a k T ha ha1 hk m l q g (t, v)) x =
      -Complex.I * oddPowerDerivative m
        (expandingTorusFunction a k (l t).1 (q t) x)
        (expandingTorusFunction a k (l t).1 v x) +
        expandingTorusFunction a k (l t).1 (g t) x := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingProfileReaction, OAI.DefocusingNLS.oddPowerDerivative

theorem OAI.DefocusingNLS.exists_expandingProfile_mild_bound line 84

Source documentation

Uniform short-slab existence for the actual varying-scale linearized potential.

theorem exists_expandingProfile_mild_bound (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 →
      ∀ (q g : C(Set.Icc (0 : ℝ) T, FourierL2)) (u₀ : FourierL2),
      (∀ t, ‖q t‖ ≤ R) →
      ∃! u : C(Set.Icc (0 : ℝ) T, FourierL2), ∀ t : Set.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