intervalIntegrable₀ — Mathlib

English

If f is periodic with period T > 0, then the integral of f over any interval of length T is independent of the starting point.

Русский

Если f периодична с периодом T > 0, то интеграл по любому интервалу длины T не зависит от начала.

LaTeX

$$$\\forall t,s: \\mathbb{R}, \\; \\int_{t}^{t+T} f(x)dx = \\int_{s}^{s+T} f(x)dx$$$

Lean4

/-- Special case of Function.Periodic.intervalIntegrable: A periodic function is interval integrable
over every interval if it is interval integrable over the period starting from zero. -/
theorem intervalIntegrable₀ (h₁f : Function.Periodic f T) (hT : 0 < T)
    (h₂f : IntervalIntegrable f MeasureTheory.volume 0 T) (a₁ a₂ : ℝ) :
    IntervalIntegrable f MeasureTheory.volume a₁ a₂ :=
  by
  apply h₁f.intervalIntegrable hT (t := 0)
  simpa

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