Matrix Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section3.hatZetaML_le_hatXiML {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) : I.hatZetaML m l t ≤ I.hatXiML m l t

The common indicator between the two cutoff envelopes implies ζ̂ ≤ ξ̂, so the large-scale coefficients have total weight at most one.

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

Zeroth-order e.Lmn.bound, with explicit n! 2ⁿ dependence.

theorem AVenhance.Infra.Section3.jMN_average_entry_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) {n : ℕ} (hn : n ≤ Nstar β) {κ : ℝ} (hκ : 0 < κ) (i j : Fin 2) : |timeAvgMat (I.jMN κ m n) 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)

Unit-time averaging preserves the entrywise bound for j.

theorem AVenhance.Infra.Section3.MatrixBounds.memory_j_bound_product {β : ℝ} (I : Ingredients β) (m n : ℕ) {κ : ℝ} (hκ : 0 < κ) : ↑n.factorial * 2 ^ n * (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 / 2)⁻¹ * (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)) = I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ * (2 * epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ * tau β I.Λ m)) ^ n

Exact cancellation of the factorial and relaxation factors.

theorem AVenhance.Infra.Section3.Kmat_entry_abs_le_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m) (t : ℝ) (i j : Fin 2) : |I.Kmat κ m t i j| ≤ κ + ↑(Nstar β) * (I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

Zeroth-order K estimate, including the molecular identity term. The ratio condition is weaker than the paper's ε² ≤ κτ/2.

theorem AVenhance.Infra.Section3.Kmat_entry_derivative_eq_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {ℓ : ℕ} (hpos : 0 < ℓ) (hℓ : ℓ ≤ Nstar β) (t : ℝ) (i j : Fin 2) : iteratedDeriv ℓ (fun (s : ℝ) => I.Kmat κ m s i j) t = ∑ n ∈ Finset.range (Nstar β), iteratedDeriv ℓ (I.LMN κ m n) t * timeAvgMat (I.jMN κ m n) i j

The positive-order derivative formula keeps only the memory factors: unit-time averages of j are constant in time.

theorem AVenhance.Infra.Section3.Kmat_entry_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m) {ℓ : ℕ} (hpos : 0 < ℓ) (hℓ : ℓ ≤ Nstar β) (t : ℝ) (i j : Fin 2) : |iteratedDeriv ℓ (fun (s : ℝ) => I.Kmat κ m s i j) t| ≤ ↑(Nstar β) * (2 ^ ℓ * I.Chat ^ 2 / tauP β I.Λ m ^ ℓ) * (I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

Positive-order e.bfK.dervs, with explicit constants, for ℓ ≤ N_*. The small-ratio premise is weaker than the printed ε² ≤ κτ/2.

theorem AVenhance.Infra.Section3.Kmat_derivative_norm_le {β C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m) {ℓ : ℕ} (hℓ : ℓ ≤ Nstar β) (t : ℝ) : ‖fun (i j : Fin 2) => iteratedDeriv ℓ (fun (s : ℝ) => I.Kmat κ m s i j) t‖ ≤ (1 + ↑(Nstar β) * 2 ^ Nstar β * C₀ ^ 3) / tauP β I.Λ m ^ ℓ * (κ + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

Uniform C(β,C₀) version for every order 0 ≤ ℓ ≤ N_*. The entrywise derivative matrix is measured in the elementwise supremum norm.

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

Smoothness of the matrix coefficient through the cutoff budget.

theorem AVenhance.Infra.Section3.MatrixBounds.iteratedDeriv_matrix_entries {F : ℝ → Fin 2 → Fin 2 → ℝ} {N ℓ : ℕ} (hf : ∀ (i j : Fin 2), ContDiff ℝ ↑↑N fun (t : ℝ) => F t i j) (hℓ : ℓ ≤ N) : iteratedDeriv ℓ F = fun (t : ℝ) (i j : Fin 2) => iteratedDeriv ℓ (fun (s : ℝ) => F s i j) t

theorem AVenhance.Infra.Section3.MatrixBounds.diffusivity_scale_eq {β : ℝ} (I : Ingredients β) (m : ℕ) : a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β) = epsilon β I.Λ m ^ (β + gamma β)

theorem AVenhance.Infra.Section3.MatrixBounds.amplitude_div_scale_eq {x β γ c : ℝ} (hx : 0 < x) (hc : 0 < c) : (x ^ (β - 2)) ^ 2 * x ^ 4 / (c * x ^ (β + γ)) = 1 / c * x ^ (β - γ)

theorem AVenhance.Infra.Section3.MatrixBounds.length_power_previous_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) : epsilon β I.Λ m ^ (β - gamma β) ≤ (1 + Ingredients.supergeoConstant β) ^ (β - gamma β) * epsilon β I.Λ (m - 1) ^ (β + gamma β)