English
If f is periodic with period T, then for any integer n, the integral over t..t+nT equals n times the integral over t..t+T.
Русский
Если f периодична с периодом T, то для любого целого n интеграл по t..t+nT равен n раз интегралу по t..t+T.
LaTeX
$$$\\int_{t}^{t+nT} f(x)dx = n\\cdot \\int_{t}^{t+T} f(x)dx, \\; n\\in\\mathbb{Z}$$$
Lean4
/-- If `f` is an integrable periodic function with period `T`, and `n` is an integer, then its
integral over `[t, t + n • T]` is `n` times its integral over `[t, t + T]`. -/
theorem intervalIntegral_add_zsmul_eq (hf : Periodic f T) (n : ℤ) (t : ℝ)
(h_int : ∀ t₁ t₂, IntervalIntegrable f MeasureSpace.volume t₁ t₂) :
∫ x in t..t + n • T, f x = n • ∫ x in t..t + T, f x := by
-- Reduce to the case `b = 0`
suffices (∫ x in 0..(n • T), f x) = n • ∫ x in 0..T, f x by
simp only [hf.intervalIntegral_add_eq t 0, (hf.zsmul n).intervalIntegral_add_eq t 0, zero_add, this]
-- First prove it for natural numbers
have : ∀ m : ℕ, (∫ x in 0..m • T, f x) = m • ∫ x in 0..T, f x := fun m ↦ by
induction m with
| zero => simp
| succ m ih =>
simp only [succ_nsmul, hf.intervalIntegral_add_eq_add 0 (m • T) h_int, ih, zero_add]
-- Then prove it for all integers
rcases n with n | n
· simp [← this n]
· conv_rhs => rw [negSucc_zsmul]
have h₀ : Int.negSucc n • T + (n + 1) • T = 0 := by simp; linarith
rw [integral_symm, ← (hf.nsmul (n + 1)).funext, neg_inj]
simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
