Regularity adapters used to construct the pointwise residual calculus data.

noncomputable def AVenhance.Infra.Section5.ResidualDataRegularity.residualJMNMode {β : ℝ} (I : Ingredients β) (m n : ℕ) (k : { k : ℤ // Odd k }) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

One shear-mode matrix term in the residual cutoff moment.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.ResidualDataRegularity.residualOddIndicesIcc (N : ℕ) : Finset { k : ℤ // Odd k }

Finite set of odd indices in a symmetric interval for the residual moment sum.

Equations

• AVenhance.Infra.Section5.ResidualDataRegularity.residualOddIndicesIcc N = ⋯.toFinset

theorem AVenhance.Infra.Section5.ResidualDataRegularity.residual_zeta_index_abs_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (t₀ t : ℝ) (k : ℤ) (ht : t ∈ Set.Icc (t₀ - 1) (t₀ + 1)) (hne : I.zetaMK m k t ≠ 0) : |↑k| ≤ (|t₀| + 1) / tau β I.Λ m + 2 / 3

theorem AVenhance.Infra.Section5.ResidualDataRegularity.residualJMNMode_eq_sum {β : ℝ} (I : Ingredients β) {m n : ℕ} (t₀ t : ℝ) (N : ℕ) (hN : (|t₀| + 1) / tau β I.Λ m + 2 < ↑N) (ht : t ∈ Set.Icc (t₀ - 1) (t₀ + 1)) : ∑' (k : { k : ℤ // Odd k }), residualJMNMode I m n k t = ∑ k ∈ residualOddIndicesIcc N, residualJMNMode I m n k t

theorem AVenhance.Infra.Section5.residual_jMN_contDiff {β : ℝ} (I : Ingredients β) (m n : ℕ) (κ : ℝ) : ContDiff ℝ (↑⊤) (I.jMN κ m n)

The explicit j_{m,n} coefficient is smooth: near each time its odd-mode series reduces to a finite sum of smooth cutoff derivatives.

theorem AVenhance.Infra.Section5.ResidualDataRegularity.residual_qMNR_entry_contDiff {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (t : ℝ) => I.qMNR κ m n r t i j

theorem AVenhance.Infra.Section5.residual_qMNR_contDiff {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) : ContDiff ℝ (↑⊤) (I.qMNR κ m n r)

Every recursive q_{m,n,r} coefficient is smooth in time.