intervalIntegral_add_eq — Mathlib

English

If f is periodic with period T > 0, then the interval integral over [t, t+T] equals the integral over [0,T] after a shift, and in particular for any t.

Русский

Если f периодична с периодом T > 0, то интервальный интеграл по [t, t+T] равен интегралу по [0,T] после смещения.

LaTeX

$$$\\int_{t}^{t+T} f(x)dx = \\int_{0}^{T} f(x)dx$ for periodic f$$

Lean4

/-- If `f` is a periodic function with period `T`, then its integral over `[t, t + T]` does not
depend on `t`. -/
theorem intervalIntegral_add_eq (hf : Periodic f T) (t s : ℝ) : ∫ x in t..t + T, f x = ∫ x in s..s + T, f x :=
  by
  rcases lt_trichotomy (0 : ℝ) T with (hT | rfl | hT)
  · exact hf.intervalIntegral_add_eq_of_pos hT t s
  · simp
  · rw [← neg_inj, ← integral_symm, ← integral_symm]
    simpa only [← sub_eq_add_neg, add_sub_cancel_right] using
      hf.neg.intervalIntegral_add_eq_of_pos (neg_pos.2 hT) (t + T) (s + T)

Похожие утверждения