Integrals of periodic functions #
In this file we prove that ∫ x in t..t + T, f x = ∫ x in s..s + T, f x
for any (not necessarily
measurable) function periodic function with period T
.
An auxiliary lemma for a more general function.periodic.interval_integral_add_eq
.
If f
is a periodic function with period T
, then its integral over [t, t + T]
does not
depend on t
.
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]
.
If f
is an integrable periodic function with period T
, and n
is an integer, then its
integral over [t, t + n • T]
is n
times its integral over [t, t + T]
.
If g : ℝ → ℝ
is periodic with period T > 0
, then for any t : ℝ
, the function
t ↦ ∫ x in 0..t, g x
is bounded below by t ↦ X + ⌊t/T⌋ • Y
for appropriate constants X
and
Y
.
If g : ℝ → ℝ
is periodic with period T > 0
, then for any t : ℝ
, the function
t ↦ ∫ x in 0..t, g x
is bounded above by t ↦ X + ⌊t/T⌋ • Y
for appropriate constants X
and
Y
.
If g : ℝ → ℝ
is periodic with period T > 0
and 0 < ∫ x in 0..T, g x
, then
t ↦ ∫ x in 0..t, g x
tends to ∞
as t
tends to ∞
.
If g : ℝ → ℝ
is periodic with period T > 0
and 0 < ∫ x in 0..T, g x
, then
t ↦ ∫ x in 0..t, g x
tends to -∞
as t
tends to -∞
.
If g : ℝ → ℝ
is periodic with period T > 0
and ∀ x, 0 < g x
, then t ↦ ∫ x in 0..t, g x
tends to ∞
as t
tends to ∞
.
If g : ℝ → ℝ
is periodic with period T > 0
and ∀ x, 0 < g x
, then t ↦ ∫ x in 0..t, g x
tends to -∞
as t
tends to -∞
.