Explicit cutoff factors in the Section 3 coefficient estimates.

The cutoff derivative budget is Nstar β; derivative estimates of a product containing ∂ⁿζ therefore require n + ℓ ≤ Nstar β. Constants are displayed rather than hidden in a β-dependent C. The memory integrals are differentiated on a fixed half-line after translation, with an integrable exponential majorant for every derivative. The matrix estimates include order zero and all orders through Nstar β; the physical diffusivity comparison is conditional on the internal-index κ bounds from the diffusivity-recursion estimates.

theorem AVenhance.Infra.Section3.zetaMK_scaled_derivative_bound {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : tau β I.Λ m ^ j * |iteratedDeriv j (I.zetaMK m k) t| ≤ I.Czeta

The cutoff bound after rescaling to the small time scale.

theorem AVenhance.Infra.Section3.zetaMK_derivative_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.zetaMK m k) t| ≤ I.Czeta / tau β I.Λ m ^ j

Unweighted form of the rescaled cutoff estimate.

theorem AVenhance.Infra.Section3.hatZetaML_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.hatZetaML m l) t| ≤ I.Chat / tauP β I.Λ m ^ j

The large-scale bound is already part of the ingredients.

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

theorem AVenhance.Infra.Section3.CutoffMemory.iteratedDeriv_iteratedDeriv (f : ℝ → ℝ) (i n : ℕ) : iteratedDeriv i (iteratedDeriv n f) = iteratedDeriv (i + n) f

def AVenhance.Infra.Section3.CutoffMemory.modeMatrix (k : ℤ) : Matrix (Fin 2) (Fin 2) ℝ

Diagonal coordinate projector associated with a shear mode.

Equations

• AVenhance.Infra.Section3.CutoffMemory.modeMatrix k = (if k % 4 = 1 then !![0, 0; 0, 1] else 0) + if k % 4 = 3 then !![1, 0; 0, 0] else 0

theorem AVenhance.Infra.Section3.CutoffMemory.modeMatrix_entry_abs_le (k : ℤ) (i j : Fin 2) : |modeMatrix k i j| ≤ 1

theorem AVenhance.Infra.Section3.CutoffMemory.zetaMK_partition {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : ∑' (k : ℤ), I.zetaMK m k t = 1

theorem AVenhance.Infra.Section3.jMN_entry_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) {n : ℕ} (hn : n ≤ Nstar β) {κ : ℝ} (hκ : 0 < κ) (t : ℝ) (i j : Fin 2) : |I.jMN κ m n t i j| ≤ 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 / ↑n.factorial * (epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ)) ^ n * (I.Czeta / tau β I.Λ m ^ n)

Entrywise version of e.jmn.bound, with an explicit constant and no hidden cutoff normalization. This is the printed (zeroth derivative) bound.

theorem AVenhance.Infra.Section3.CutoffMemory.iteratedDeriv_congr_nhds {f g : ℝ → ℝ} {t : ℝ} (h : f =ᶠ[nhds t] g) (ℓ : ℕ) : iteratedDeriv ℓ f t = iteratedDeriv ℓ g t

theorem AVenhance.Infra.Section3.CutoffMemory.odd_mode_cutoffs_locally_single {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : ∃ (k : ℤ) (hk : Odd k), ∀ᶠ (s : ℝ) in nhds t, ∀ (k' : { k : ℤ // Odd k }), k' ≠ ⟨k, hk⟩ → I.zetaMK m (↑k') s = 0

theorem AVenhance.Infra.Section3.CutoffMemory.jMN_locally_single_mode {β : ℝ} (I : Ingredients β) (m n : ℕ) (κ t : ℝ) (i j : Fin 2) : ∃ (k : ℤ), Odd k ∧ (fun (s : ℝ) => I.jMN κ m n s i j) =ᶠ[nhds t] fun (s : ℝ) => 2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2 / ↑n.factorial * (epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ)) ^ n * (I.zetaMK m k s * iteratedDeriv n (I.zetaMK m k) s) * modeMatrix k i j

An odd mode can be chosen so that all other odd cutoffs vanish on a neighborhood of the given time. The gap between odd supports is essential.

theorem AVenhance.Infra.Section3.polynomial_exp_abs_le (n : ℕ) {x : ℝ} (hx : x ≤ 0) : |x ^ n * Real.exp x| ≤ ↑n.factorial * 2 ^ n * Real.exp (x / 2)

A convenient exponential majorant for every polynomial memory kernel. The factor two sacrifices sharpness and avoids an improper gamma integral.

theorem AVenhance.Infra.Section3.CutoffMemory.exp_memory_integrable {ρ : ℝ} (hρ : 0 < ρ) (t : ℝ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (ρ * (s - t))) (Set.Iic t) MeasureTheory.volume

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

theorem AVenhance.Infra.Section3.LMN_memory_integral_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n : ℕ) (l : ℤ) (t : ℝ) : |∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * (4 * Real.pi ^ 2 * κ * (s - t) / epsilon β I.Λ m ^ 2) ^ n * Real.exp (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (s - t))| ≤ ↑n.factorial * 2 ^ n * (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 / 2)⁻¹

Each memory integral has an explicit factorial bound. No integrability premise is assumed: an integrable exponential majorant suffices.

def AVenhance.Infra.Section3.CutoffMemory.cutoffPair (f : ℝ → ℝ) (u : ℝ) : ℝ → ℝ

Product of a time cutoff and its translate by a fixed lag.

Equations

• AVenhance.Infra.Section3.CutoffMemory.cutoffPair f u t = f t * f (t + u)

theorem AVenhance.Infra.Section3.CutoffMemory.cutoffPair_smooth {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (u : ℝ) : ContDiff ℝ (↑⊤) (cutoffPair f u)

theorem AVenhance.Infra.Section3.CutoffMemory.cutoffPair_derivative_bound {f : ℝ → ℝ} {N j : ℕ} {B τ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) (u t : ℝ) : |iteratedDeriv j (cutoffPair f u) t| ≤ 2 ^ j * B ^ 2 / τ ^ j

theorem AVenhance.Infra.Section3.CutoffMemory.cutoffPair_derivative_continuous_shift {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (t : ℝ) : Continuous fun (u : ℝ) => iteratedDeriv j (cutoffPair f u) t

noncomputable def AVenhance.Infra.Section3.CutoffMemory.pairMemory (f : ℝ → ℝ) (ρ : ℝ) (n j : ℕ) (t : ℝ) : ℝ

Past-lag exponential memory integral of a derivative of a cutoff pair.

Equations

• AVenhance.Infra.Section3.CutoffMemory.pairMemory f ρ n j t = ∫ (u : ℝ) in Set.Iic 0, iteratedDeriv j (AVenhance.Infra.Section3.CutoffMemory.cutoffPair f u) t * ((ρ * u) ^ n * Real.exp (ρ * u))

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_integrand_bound {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) (t : ℝ) {u : ℝ} (hu : u ≤ 0) : ‖iteratedDeriv j (cutoffPair f u) t * ((ρ * u) ^ n * Real.exp (ρ * u))‖ ≤ 2 ^ j * B ^ 2 / τ ^ j * (↑n.factorial * 2 ^ n) * Real.exp (ρ / 2 * u)

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_integrand_continuous {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (ρ : ℝ) (n j : ℕ) (t : ℝ) : Continuous fun (u : ℝ) => iteratedDeriv j (cutoffPair f u) t * ((ρ * u) ^ n * Real.exp (ρ * u))

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_integrable {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) (t : ℝ) : MeasureTheory.IntegrableOn (fun (u : ℝ) => iteratedDeriv j (cutoffPair f u) t * ((ρ * u) ^ n * Real.exp (ρ * u))) (Set.Iic 0) MeasureTheory.volume

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_hasDerivAt {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j < N) (t : ℝ) : HasDerivAt (pairMemory f ρ n j) (pairMemory f ρ n (j + 1) t) t

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_derivative {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) : iteratedDeriv j (pairMemory f ρ n 0) = pairMemory f ρ n j

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_abs_le {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) (t : ℝ) : |pairMemory f ρ n j t| ≤ 2 ^ j * B ^ 2 / τ ^ j * (↑n.factorial * 2 ^ n) * (ρ / 2)⁻¹

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_continuous {f : ℝ → ℝ} {N j n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) (hj : j ≤ N) : Continuous (pairMemory f ρ n j)

theorem AVenhance.Infra.Section3.CutoffMemory.pairMemory_contDiff {f : ℝ → ℝ} {N n : ℕ} {B τ ρ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hB : 0 ≤ B) (hτ : 0 < τ) (hρ : 0 < ρ) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ B / τ ^ j) : ContDiff ℝ (↑↑N) (pairMemory f ρ n 0)

theorem AVenhance.Infra.Section3.CutoffMemory.memory_pair_translation (f : ℝ → ℝ) (ρ : ℝ) (n : ℕ) (t : ℝ) : f t * ∫ (s : ℝ) in Set.Iic t, f s * ((ρ * (s - t)) ^ n * Real.exp (ρ * (s - t))) = pairMemory f ρ n 0 t

theorem AVenhance.Infra.Section3.CutoffMemory.hat_mode_cutoffs_locally_single {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∃ (l : ℤ), ∀ᶠ (s : ℝ) in nhds t, ∀ (l' : ℤ), l' ≠ l → I.hatZetaML m l' s = 0

theorem AVenhance.Infra.Section3.CutoffMemory.LMN_locally_pairMemory {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) (t : ℝ) : ∃ (l : ℤ), I.LMN κ m n =ᶠ[nhds t] pairMemory (I.hatZetaML m l) (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) n 0

theorem AVenhance.Infra.Section3.LMN_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n : ℕ) {ℓ : ℕ} (hℓ : ℓ ≤ Nstar β) (t : ℝ) : |iteratedDeriv ℓ (I.LMN κ m n) t| ≤ 2 ^ ℓ * I.Chat ^ 2 / tauP β I.Λ m ^ ℓ * (↑n.factorial * 2 ^ n) * (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 / 2)⁻¹

e.Lmn.bound for the actual memory sum, including every positive order allowed by the cutoff budget. Constants retain the factorial and Leibniz factors explicitly.

theorem AVenhance.Infra.Section3.LMN_derivative_paper_bound {β C₀ : ℝ} (I : Ingredients β) (hcutoff : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n ℓ : ℕ} (hn : n ≤ Nstar β) (hℓ : ℓ ≤ Nstar β) (t : ℝ) : |iteratedDeriv ℓ (I.LMN κ m n) t| ≤ ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * C₀ ^ 2 / (2 * Real.pi ^ 2) * (epsilon β I.Λ m ^ 2 / κ) / tauP β I.Λ m ^ ℓ

The paper-size bound with one constant uniform in both indices. Only I.Chat ≤ C₀ is needed for the memory coefficient.

theorem AVenhance.Infra.Section3.LMN_contDiff {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n : ℕ) : ContDiff ℝ (↑↑(Nstar β)) (I.LMN κ m n)

The memory coefficient is C^{N_*} in time.