Quantitative slow variation of the Section 3 forcing cutoffs.

theorem AVenhance.Infra.Section3.zetaProd_deriv_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : |deriv (I.zetaProd m k) t| ≤ (I.Czeta + I.Chat) / tau β I.Λ m

The product forcing cutoff has a global derivative bound at the small cutoff scale. The large cutoff contributes Chat / tauP, and tauP ≥ tau; the small cutoff contributes Czeta / tau.

theorem AVenhance.Infra.Section3.FluxEnergyCutoff.expKernel_integral_Iic {ρ t : ℝ} (hρ : 0 < ρ) : ∫ (s : ℝ) in Set.Iic t, Real.exp (ρ * (s - t)) = ρ⁻¹

theorem AVenhance.Infra.Section3.FluxEnergyCutoff.corrTime_forcingError_eq_deriv_integral {β : ℝ} (I : Ingredients β) {m : ℕ} (κ ρ : ℝ) (k : ℤ) (t : ℝ) (hρ : ρ = 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) : I.zetaProd m k t - ρ * I.corrTime κ m k t = ∫ (s : ℝ) in Set.Iic t, deriv (I.zetaProd m k) s * Real.exp (ρ * (s - t))

Integration by parts in the defining memory integral: its ODE defect is the exponentially weighted derivative of the forcing cutoff.

theorem AVenhance.Infra.Section3.corrTime_forcingError_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) : |I.zetaProd m k t - 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * I.corrTime κ m k t| ≤ (I.Czeta + I.Chat) / (4 * Real.pi ^ 2) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The memory tracks its instantaneous forcing with error bounded by the forcing's variation over one relaxation time. This is the quantitative integration-by-parts step only sketched at source lines 3399--3416.