intervalIntegral_add_eq_of_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- An auxiliary lemma for a more general `Function.Periodic.intervalIntegral_add_eq`. -/
theorem intervalIntegral_add_eq_of_pos (hf : Periodic f T) (hT : 0 < T) (t s : ℝ) :
    ∫ x in t..t + T, f x = ∫ x in s..s + T, f x :=
  by
  simp only [integral_of_le, hT.le, le_add_iff_nonneg_right]
  haveI : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume := ⟨fun c s _ => measure_preimage_add _ _ _⟩
  apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples T)
  exacts [isAddFundamentalDomain_Ioc hT t, isAddFundamentalDomain_Ioc hT s, hf.map_vadd_zmultiples]

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