ExpandingDecayingDuhamel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The decaying cutoff residual in the moving-scale Duhamel estimate

The extra exp(-t) in the residual is integrable. Its propagated contribution therefore retains the free decay with no factor depending on the slab length.

theorem OAI.DefocusingNLS.integral_exp_neg_Icc line 15

theorem OAI.DefocusingNLS.expandingDuhamel_fast_source_norm_le line 28

Source documentation

A source with the actual cutoff decay gives a free-decaying response.

theorem expandingDuhamel_fast_source_norm_le (a b k L t C : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (ht : 0 ≤ t) (hC : 0 ≤ C)
    (r : ℝ → FourierL2)
    (hbound : ∀ τ ∈ Icc 0 t, ‖r τ‖ ≤ C * Real.exp (-(2 + a) * τ / 2)) :
    ‖expandingDuhamel a b k L ha hk hL t r‖ ≤ C * Real.exp (-a * t / 2) := by
…

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