intervalIntegral_add_eq_add — Mathlib

English

For periodic f, the integral over [t, s+T] equals the sum of integrals over [t,s] and [t,t+T].

Русский

Для периодической f интеграл по [t, s+T] равен сумме интегралов по [t,s] и [t,t+T].

LaTeX

$$$\\int_{t}^{s+T} f(x)dx = \\bigl(\\int_{t}^{s} f(x)dx\\bigr) + \\bigl(\\int_{t}^{t+T} f(x)dx\\bigr)$$$

Lean4

/-- If `f` is an integrable periodic function with period `T`, then its integral over `[t, s + T]`
is the sum of its integrals over the intervals `[t, s]` and `[t, t + T]`. -/
theorem intervalIntegral_add_eq_add (hf : Periodic f T) (t s : ℝ)
    (h_int : ∀ t₁ t₂, IntervalIntegrable f MeasureSpace.volume t₁ t₂) :
    ∫ x in t..s + T, f x = (∫ x in t..s, f x) + ∫ x in t..t + T, f x := by
  rw [hf.intervalIntegral_add_eq t s, integral_add_adjacent_intervals (h_int t s) (h_int s _)]

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