Theorems · Theorem · measure theory

Function.Periodic.intervalIntegral_add_eq

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
  Function.Periodic f T → ∀ (t s : ℝ), ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

7 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace