The explicit j_{m,n} coefficients have the corrected period 4τ_m.

def AVenhance.Infra.Section3.JMNPeriodicity.oddIndexShiftFour : { k : ℤ // Odd k } ≃ { k : ℤ // Odd k }

Translate an odd integer index by four, preserving its parity.

Equations

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

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

One odd-index matrix term in the cutoff-derivative moment sum.

Equations

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

theorem AVenhance.Infra.Section3.JMNPeriodicity.zetaMK_add_four {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) : I.zetaMK m (k + 4) (t + 4 * tau β I.Λ m) = I.zetaMK m k t

theorem AVenhance.Infra.Section3.JMNPeriodicity.iteratedDeriv_zetaMK_add_four {β : ℝ} (I : Ingredients β) {m n : ℕ} (k : ℤ) (t : ℝ) : iteratedDeriv n (I.zetaMK m (k + 4)) (t + 4 * tau β I.Λ m) = iteratedDeriv n (I.zetaMK m k) t

theorem AVenhance.Infra.Section3.JMNPeriodicity.jMNSummand_shift {β : ℝ} (I : Ingredients β) {m n : ℕ} (k : { k : ℤ // Odd k }) (t : ℝ) : jMNSummand I m n (oddIndexShiftFour k) (t + 4 * tau β I.Λ m) = jMNSummand I m n k t

theorem AVenhance.Infra.Section3.jMN_period_four_tau {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (n : ℕ) : Function.Periodic (I.jMN κ m n) (4 * tau β I.Λ m)

Each explicit coefficient j_{m,n} has period 4τ_m.