Local finiteness and continuity of the explicit j_{m,n} coefficient.

noncomputable def AVenhance.Infra.Section3.JMNRegularity.jMNSummand' {β : ℝ} (I : Ingredients β) (m n : ℕ) (k : { k : ℤ // Odd k }) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

One odd-index matrix term used to establish regularity of the moment sum.

Equations

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

theorem AVenhance.Infra.Section3.JMNRegularity.zetaMK_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

noncomputable def AVenhance.Infra.Section3.JMNRegularity.oddIndicesIcc (N : ℕ) : Finset { k : ℤ // Odd k }

Finite set of odd integer indices in a symmetric interval.

Equations

• AVenhance.Infra.Section3.JMNRegularity.oddIndicesIcc N = ⋯.toFinset

theorem AVenhance.Infra.Section3.JMNRegularity.jMNSummand_eq_finite_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 }), jMNSummand' I m n k t = ∑ k ∈ oddIndicesIcc N, jMNSummand' I m n k t

theorem AVenhance.Infra.Section3.JMNRegularity.jMNSummand_continuous {β : ℝ} (I : Ingredients β) (m n : ℕ) (k : { k : ℤ // Odd k }) : Continuous fun (t : ℝ) => jMNSummand' I m n k t

theorem AVenhance.Infra.Section3.jMN_continuous {β : ℝ} (I : Ingredients β) (m n : ℕ) (κ : ℝ) : Continuous (I.jMN κ m n)

The locally finite odd-mode series defining j_{m,n} is continuous in time.