The unit-time average is also the average over an integer number of 4τ_m periods.

theorem AVenhance.Infra.Section3.four_tau_reciprocal_nat {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : ∃ (N : ℕ), ↑N * (4 * tau β I.Λ m) = 1

The reciprocal of 4τ_m is a positive integer.

theorem AVenhance.Infra.Section3.intervalIntegral_unit_eq_period_mul {f : ℝ → ℝ} {P : ℝ} {N : ℕ} (hperiodic : Function.Periodic f P) (hcont : Continuous f) (hunit : ↑N * P = 1) : ∫ (t : ℝ) in 0..1, f t = ↑N * ∫ (t : ℝ) in 0..P, f t

Integrating a continuous periodic function over an integer number of periods.

theorem AVenhance.Infra.Section3.jMN_average_eq_period_average {β : ℝ} (I : Ingredients β) {m n : ℕ} (hm : 1 ≤ m) (κ : ℝ) (i j : Fin 2) : ∫ (t : ℝ) in 0..1, I.jMN κ m n t i j = (4 * tau β I.Λ m)⁻¹ * ∫ (t : ℝ) in 0..4 * tau β I.Λ m, I.jMN κ m n t i j

The entries of j_{m,n} have the same average over a single 4τ_m cell as on [0,1]. The equality uses the exact integer subdivision encoded in tau_m.