Continuity of the explicit single-mode memory integral.

theorem AVenhance.Infra.Section3.CorrTimeRegularity.zetaMK_hasCompactSupport {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) : HasCompactSupport (I.zetaMK m k)

theorem AVenhance.Infra.Section3.zetaProd_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) : Continuous (I.zetaProd m k)

theorem AVenhance.Infra.Section3.zetaProd_hasCompactSupport {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) : HasCompactSupport (I.zetaProd m k)

theorem AVenhance.Infra.Section3.zetaProd_exp_continuous_compactSupport {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) : (Continuous fun (s : ℝ) => I.zetaProd m k s * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * s)) ∧ HasCompactSupport fun (s : ℝ) => I.zetaProd m k s * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * s)

Each mode's temporal forcing is continuous and compactly supported.

theorem AVenhance.Infra.Section3.corrTime_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) : Continuous (I.corrTime κ m k)

The corrTime is continuous in time for every positive-scale mode.

theorem AVenhance.Infra.Section3.zetaProd_contDiff {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) : ContDiff ℝ (↑⊤) (I.zetaProd m k)

Smoothness of a single-mode forcing in the cutoff data.

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

theorem AVenhance.Infra.Section3.corrTime_hasDerivAt {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) : HasDerivAt (I.corrTime κ m k) (I.zetaProd m k t - 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * I.corrTime κ m k t) t

The explicit memory coefficient solves its scalar relaxation ODE.

theorem AVenhance.Infra.Section3.corrTime_contDiff_two {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) : ContDiff ℝ 2 (I.corrTime κ m k)

The memory integral is C² in time; this is enough for the joint C² regularity of the single-mode corrector.