Corrector decay after its forcing support (e.corrbounds.Chi.decay)

The explicit one-mode corrector χ_{m,k} = -corrTime · u_{m,k} is driven by ζ̂_{m,l_k} ζ_{m,k}, supported in [(k - 2/3) τ_m, (k + 2/3) τ_m]. For t ≥ (k + 3/4) τ_m the memory integral corrTime is at most (4/3) τ_m exp(-(4π²κ/ε_m²) τ_m / 12) (enhance.tex 2860–2900; π²κτ_m/(3ε_m²) is the printed exponent).

theorem AVenhance.Infra.Section5.Contracts.sb_zetaMK_eq_zero_of_not_mem {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) {s : ℝ} (hs : s ∉ Set.Icc ((↑k - 2 / 3) * tau β I.Λ m) ((↑k + 2 / 3) * tau β I.Λ m)) : I.zetaMK m k s = 0

ζ_{m,k}(s) vanishes outside [(k - 2/3) τ_m, (k + 2/3) τ_m].

theorem AVenhance.Infra.Section5.Contracts.sb_corrTime_nonneg_le_decay {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 ≤ κ) (k : ℤ) {t : ℝ} (ht : (↑k + 3 / 4) * tau β I.Λ m ≤ t) : 0 ≤ I.corrTime κ m k t ∧ I.corrTime κ m k t ≤ 4 / 3 * tau β I.Λ m * Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (tau β I.Λ m / 12)))

Corrector decay (e.corrbounds.Chi.decay): after (k + 3/4) τ_m the memory integral is exponentially small.