ExpandingDuhamel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Inhomogeneous propagation in the exact expanding Sobolev norms

The forcing at time τ is represented in Y_(L exp(τ/2)). Its free transport therefore lands in the same final space Y_(L exp(t/2)) for every τ ∈ [0,t]. The estimate keeps the exact exponential kernel and is uniform in L ≥ 1.

def OAI.DefocusingNLS.expandingDuhamelIntegrand line 17
def OAI.DefocusingNLS.expandingDuhamel line 25
theorem OAI.DefocusingNLS.expandingDuhamelIntegrand_of_mem line 30
theorem OAI.DefocusingNLS.expandingDuhamel_destination line 39
Source documentation
Every forcing time is transported into the prescribed final expanding torus.
```
theorem expandingDuhamel_destination (L t τ : ℝ) :
    expandingRadius (expandingRadius L τ) (t - τ) = expandingRadius L t := by
…
```
Mentions: OAI.DefocusingNLS.expandingRadius
theorem OAI.DefocusingNLS.continuousOn_expandingDuhamelIntegrand line 45
theorem OAI.DefocusingNLS.integrableOn_expandingDuhamelIntegrand line 66

theorem OAI.DefocusingNLS.expandingDuhamel_norm_le line 73

Source documentation

Variation of constants has the manuscript's exp(-a (t-τ)/2) bound.

theorem expandingDuhamel_norm_le (a b k L : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
    (t : ℝ) (r : ℝ → FourierL2) (hr : ContinuousOn r (Icc 0 t)) :
    ‖expandingDuhamel a b k L ha hk hL t r‖ ≤
      ∫ τ in Icc 0 t, Real.exp (-a * (t - τ) / 2) * ‖r τ‖ := by
…

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

theorem OAI.DefocusingNLS.expandingDuhamel_sub line 88

Source documentation

The inhomogeneous operator is linear in continuous forcing histories.

theorem expandingDuhamel_sub (a b k L : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
    (t : ℝ) (r q : ℝ → FourierL2)
    (hr : ContinuousOn r (Icc 0 t)) (hq : ContinuousOn q (Icc 0 t)) :
    expandingDuhamel a b k L ha hk hL t (fun τ => r τ - q τ) =
      expandingDuhamel a b k L ha hk hL t r - expandingDuhamel a b k L ha hk hL t q := by
…

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

theorem OAI.DefocusingNLS.expandingDuhamel_sub_norm_le line 102

Source documentation

The same exponential kernel controls perturbations of the forcing history.

theorem expandingDuhamel_sub_norm_le (a b k L : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
    (t : ℝ) (r q : ℝ → FourierL2)
    (hr : ContinuousOn r (Icc 0 t)) (hq : ContinuousOn q (Icc 0 t)) :
    ‖expandingDuhamel a b k L ha hk hL t r - expandingDuhamel a b k L ha hk hL t q‖ ≤
      ∫ τ in Icc 0 t, Real.exp (-a * (t - τ) / 2) * ‖r τ - q τ‖ := by
…

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

theorem OAI.DefocusingNLS.expandingDuhamel_norm_le_mul line 112

Source documentation

A bounded forcing gives a scale-independent short-time estimate.

theorem expandingDuhamel_norm_le_mul (a b k L : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
    (t C : ℝ) (ht : 0 ≤ t) (r : ℝ → FourierL2)
    (hr : ContinuousOn r (Icc 0 t)) (hbound : ∀ τ ∈ Icc 0 t, ‖r τ‖ ≤ C) :
    ‖expandingDuhamel a b k L ha hk hL t r‖ ≤ t * C := by
…

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