Integrals of periodic functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that the half-open interval Ioc t (t + T) in ℝ is a fundamental domain of
the action of the subgroup ℤ ∙ T on ℝ.
A consequence is add_circle.measure_preserving_mk: the covering map from ℝ to the "additive
circle" ℝ ⧸ (ℤ ∙ T) is measure-preserving, with respect to the restriction of Lebesgue measure to
Ioc t (t + T) (upstairs) and with respect to Haar measure (downstairs).
Another consequence (function.periodic.interval_integral_add_eq and related declarations) is that
∫ x in t..t + T, f x = ∫ x in s..s + T, f x for any (not necessarily measurable) function with
period T.
Equip the "additive circle" ℝ ⧸ (ℤ ∙ T) with, as a standard measure, the Haar measure of total
mass T
Equations
The covering map from ℝ to the "additive circle" ℝ ⧸ (ℤ ∙ T) is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass T)
on the additive circle, and with respect to the restriction of Lebsegue measure on ℝ to an
interval (t, t + T].
The isomorphism add_circle T ≃ Ioc a (a + T) whose inverse is the natural quotient map,
as an equivalence of measurable spaces.
Equations
- add_circle.measurable_equiv_Ioc T a = {to_equiv := {to_fun := (add_circle.equiv_Ioc T a).to_fun, inv_fun := (add_circle.equiv_Ioc T a).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
The isomorphism add_circle T ≃ Ico a (a + T) whose inverse is the natural quotient map,
as an equivalence of measurable spaces.
Equations
- add_circle.measurable_equiv_Ico T a = {to_equiv := {to_fun := (add_circle.equiv_Ico T a).to_fun, inv_fun := (add_circle.equiv_Ico T a).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
The lower integral of a function over add_circle T is equal to the lower integral over an
interval (t, t + T] in ℝ of its lift to ℝ.
The integral of an almost-everywhere strongly measurable function over add_circle T is equal
to the integral over an interval (t, t + T] in ℝ of its lift to ℝ.
The integral of an almost-everywhere strongly measurable function over add_circle T is equal
to the integral over an interval (t, t + T] in ℝ of its lift to ℝ.
Equations
The covering map from ℝ to the "unit additive circle" ℝ ⧸ ℤ is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass 1)
on the additive circle, and with respect to the restriction of Lebsegue measure on ℝ to an
interval (t, t + 1].
The integral of a measurable function over unit_add_circle is equal to the integral over an
interval (t, t + 1] in ℝ of its lift to ℝ.
The integral of an almost-everywhere strongly measurable function over unit_add_circle is
equal to the integral over an interval (t, t + 1] in ℝ of its lift to ℝ.
The integral of an almost-everywhere strongly measurable function over unit_add_circle is
equal to the integral over an interval (t, t + 1] in ℝ of its lift to ℝ.
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 -∞.