# mathlib3documentation

measure_theory.integral.periodic

# 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.

@[protected, instance]
noncomputable def add_circle.measurable_space {a : } :
Equations
@[protected, instance]
@[protected, measurability]
theorem add_circle.measurable_mk' {a : } :
theorem is_add_fundamental_domain_Ioc {T : } (hT : 0 < T) (t : ) (μ : . "volume_tac") :
μ
theorem is_add_fundamental_domain_Ioc' {T : } (hT : 0 < T) (t : ) (μ : . "volume_tac") :
@[protected, instance]
noncomputable def add_circle.measure_space (T : ) [hT : fact (0 < T)] :

Equip the "additive circle" ℝ ⧸ (ℤ ∙ T) with, as a standard measure, the Haar measure of total mass T

Equations
@[protected, simp]
theorem add_circle.measure_univ (T : ) [hT : fact (0 < T)] :
@[protected, instance]
@[protected, instance]
@[protected]
theorem add_circle.measure_preserving_mk (T : ) [hT : fact (0 < T)] (t : ) :

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].

theorem add_circle.volume_closed_ball (T : ) [hT : fact (0 < T)] {x : add_circle T} (ε : ) :
@[protected, instance]
Equations
noncomputable def add_circle.measurable_equiv_Ioc (T : ) [hT : fact (0 < T)] (a : ) :
≃ᵐ (set.Ioc a (a + T))

The isomorphism add_circle T ≃ Ioc a (a + T) whose inverse is the natural quotient map, as an equivalence of measurable spaces.

Equations
noncomputable def add_circle.measurable_equiv_Ico (T : ) [hT : fact (0 < T)] (a : ) :
≃ᵐ (set.Ico a (a + T))

The isomorphism add_circle T ≃ Ico a (a + T) whose inverse is the natural quotient map, as an equivalence of measurable spaces.

Equations
@[protected]
theorem add_circle.lintegral_preimage (T : ) [hT : fact (0 < T)] (t : ) (f : ennreal) :
∫⁻ (a : ) in (t + T), f a = ∫⁻ (b : , f b

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 ℝ.

@[protected]
theorem add_circle.integral_preimage (T : ) [hT : fact (0 < T)] {E : Type u_1} [ E] (t : ) (f : E) :
(a : ) in (t + T), f a = (b : , f b

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 ℝ.

@[protected]
theorem add_circle.interval_integral_preimage (T : ) [hT : fact (0 < T)] {E : Type u_1} [ E] (t : ) (f : E) :
(a : ) in t..t + T, f a = (b : , f b

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 ℝ.

@[protected, instance]
Equations
@[protected, simp]
@[protected, instance]
@[protected]

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].

@[protected]
theorem unit_add_circle.lintegral_preimage (t : )  :
∫⁻ (a : ) in (t + 1), f a = ∫⁻ (b : unit_add_circle), f b

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 ℝ.

@[protected]
theorem unit_add_circle.integral_preimage {E : Type u_1} [ E] (t : ) (f : unit_add_circle E) :
(a : ) in (t + 1), f a = (b : unit_add_circle), f b

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 ℝ.

@[protected]
theorem unit_add_circle.interval_integral_preimage {E : Type u_1} [ E] (t : ) (f : unit_add_circle E) :
(a : ) in t..t + 1, f a = (b : unit_add_circle), f b

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 ℝ.

theorem function.periodic.interval_integral_add_eq_of_pos {E : Type u_1} [ E] {f : E} {T : } (hf : T) (hT : 0 < T) (t s : ) :
(x : ) in t..t + T, f x = (x : ) in s..s + T, f x

An auxiliary lemma for a more general function.periodic.interval_integral_add_eq.

theorem function.periodic.interval_integral_add_eq {E : Type u_1} [ E] {f : E} {T : } (hf : 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.

theorem function.periodic.interval_integral_add_eq_add {E : Type u_1} [ E] {f : E} {T : } (hf : T) (t s : ) (h_int : (t₁ t₂ : ), ) :
(x : ) in t..s + T, f x = ( (x : ) in t..s, f x) + (x : ) in t..t + T, f x

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].

theorem function.periodic.interval_integral_add_zsmul_eq {E : Type u_1} [ E] {f : E} {T : } (hf : T) (n : ) (t : ) (h_int : (t₁ t₂ : ), ) :
(x : ) in t..t + n T, f x = n (x : ) in t..t + T, f x

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].

theorem function.periodic.Inf_add_zsmul_le_integral_of_pos {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (hT : 0 < T) (t : ) :
has_Inf.Inf ((λ (t : ), (x : ) in 0..t, g x) '' T) + t / T (x : ) in 0..T, g x (x : ) in 0..t, g x

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.

theorem function.periodic.integral_le_Sup_add_zsmul_of_pos {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (hT : 0 < T) (t : ) :
(x : ) in 0..t, g x has_Sup.Sup ((λ (t : ), (x : ) in 0..t, g x) '' T) + t / T (x : ) in 0..T, g x

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.

theorem function.periodic.tendsto_at_top_interval_integral_of_pos {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (h₀ : 0 < (x : ) in 0..T, g x) (hT : 0 < T) :

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 ∞.

theorem function.periodic.tendsto_at_bot_interval_integral_of_pos {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (h₀ : 0 < (x : ) in 0..T, g x) (hT : 0 < T) :

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 -∞.

theorem function.periodic.tendsto_at_top_interval_integral_of_pos' {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (h₀ : (x : ), 0 < g x) (hT : 0 < T) :

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 ∞.

theorem function.periodic.tendsto_at_bot_interval_integral_of_pos' {T : } {g : } (hg : T) (h_int : (t₁ t₂ : ), ) (h₀ : (x : ), 0 < g x) (hT : 0 < T) :

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 -∞.