C^∞ regularity of the memory coefficients L_{m,n} and of 𝐊_m

The memory coefficient L^κ_{m,n}(t) = ∑_l ζ̂_{m,l}(t) ∫_{-∞}^t ζ̂_{m,l}(s) (ρ(s-t))ⁿ e^{ρ(s-t)} ds is a locally finite sum. Each term is f(t) · (K ⋆ f)(t) with f = ζ̂_{m,l} smooth with compact support and K the locally integrable memory kernel, hence smooth by the convolution theorem.

Locally finite sums of smooth functions

theorem AVenhance.Infra.Section5.RelativeError.contDiff_tsum_of_locallyFinite {E : Type u_1} {F : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {g : ι → E → F} (hg : ∀ (i : ι), ContDiff ℝ n (g i)) (hloc : ∀ (x : E), ∃ (s : Finset ι), ∀ᶠ (y : E) in nhds x, ∀ i ∉ s, g i y = 0) : ContDiff ℝ n fun (y : E) => ∑' (i : ι), g i y

A locally finite sum of C^n functions is C^n.

theorem AVenhance.Infra.Section5.RelativeError.exists_finset_far {T : ℝ} (hT : 0 < T) (R t : ℝ) : ∃ (S : Finset ℤ), ∀ (s : ℝ), |s - t| < 1 → ∀ l ∉ S, R < |s - ↑l * T|

Around every time t, only finitely many lattice points l T lie within R + 1 of t; any l outside this finite set is at distance more than R from every s with |s - t| < 1.

Support of the cutoff families

theorem AVenhance.Infra.Section5.RelativeError.hatZetaML_abs_le_of_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatZetaML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ 1 / 2 * tauPP β I.Λ m

ζ̂_{m,l}(t) ≠ 0 forces |t - l τ''_m| ≤ τ''_m / 2.

theorem AVenhance.Infra.Section5.RelativeError.hatXiML_abs_le_of_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ 1 / 2 * tauPP β I.Λ m + tauP β I.Λ m

ξ̂_{m,l}(t) ≠ 0 forces |t - l τ''_m| ≤ τ''_m / 2 + τ'_m.

theorem AVenhance.Infra.Section5.RelativeError.hatZetaML_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (l : ℤ) : ContDiff ℝ (↑⊤) (I.hatZetaML m l)

Each ζ̂_{m,l} is smooth.

theorem AVenhance.Infra.Section5.RelativeError.hatXiML_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (l : ℤ) : ContDiff ℝ (↑⊤) (I.hatXiML m l)

Each ξ̂_{m,l} is smooth.

theorem AVenhance.Infra.Section5.RelativeError.hatZetaML_hasCompactSupport {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) : HasCompactSupport (I.hatZetaML m l)

Each ζ̂_{m,l} has compact support.

theorem AVenhance.Infra.Section5.RelativeError.exists_finset_hatXi_vanish {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∃ (S : Finset ℤ), ∀ (s : ℝ), |s - t| < 1 → ∀ l ∉ S, I.hatXiML m l s = 0

The family ξ̂_{m,l}, ζ̂_{m,l} is locally finite in l, uniformly on unit time windows.

theorem AVenhance.Infra.Section5.RelativeError.exists_finset_hatZeta_vanish {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∃ (S : Finset ℤ), ∀ (s : ℝ), |s - t| < 1 → ∀ l ∉ S, I.hatZetaML m l s = 0

The memory kernel as a convolution

noncomputable def AVenhance.Infra.Section5.RelativeError.memKernel (ρ : ℝ) (n : ℕ) : ℝ → ℝ

The memory kernel y ↦ 1_{y ≥ 0} (-ρ y)ⁿ e^{-ρ y}.

Equations

• AVenhance.Infra.Section5.RelativeError.memKernel ρ n = (Set.Ici 0).indicator fun (y : ℝ) => (-(ρ * y)) ^ n * Real.exp (-(ρ * y))

theorem AVenhance.Infra.Section5.RelativeError.memKernel_locallyIntegrable (ρ : ℝ) (n : ℕ) : MeasureTheory.LocallyIntegrable (memKernel ρ n) MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.memory_integral_eq_convolution (f : ℝ → ℝ) (ρ : ℝ) (n : ℕ) (t : ℝ) : ∫ (s : ℝ) in Set.Iic t, f s * (ρ * (s - t)) ^ n * Real.exp (ρ * (s - t)) = MeasureTheory.convolution (memKernel ρ n) f (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume t

The memory integral is a convolution with the memory kernel.

theorem AVenhance.Infra.Section5.RelativeError.memory_term_contDiff {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hcs : HasCompactSupport f) (ρ : ℝ) (n : ℕ) : ContDiff ℝ ↑⊤ fun (t : ℝ) => f t * ∫ (s : ℝ) in Set.Iic t, f s * (ρ * (s - t)) ^ n * Real.exp (ρ * (s - t))

The f(t) ∫_{-∞}^t f(s) (ρ(s-t))ⁿ e^{ρ(s-t)} ds of a smooth compactly supported f is smooth.

Smoothness of L_{m,n} and 𝐊_m

theorem AVenhance.Infra.Section5.RelativeError.LMN_contDiff_top {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (_hκ : 0 < κ) (n : ℕ) : ContDiff ℝ (↑⊤) (I.LMN κ m n)

The memory coefficient L^κ_{m,n} is C^∞ in time.

theorem AVenhance.Infra.Section5.RelativeError.Kmat_contDiff_top {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) : ContDiff ℝ (↑⊤) (I.Kmat κ m)

The matrix coefficient 𝐊^κ_m is C^∞ in time.