# mathlibdocumentation

measure_theory.integral.periodic

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

theorem is_add_fundamental_domain_Ioc {T : } (hT : 0 < T) (t : ) (μ : . "volume_tac") :
μ
theorem function.periodic.interval_integral_add_eq_of_pos {E : Type u_1} [normed_group E] [ 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} [normed_group E] [ 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} [normed_group E] [ 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} [normed_group E] [ 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) :
filter.tendsto (λ (t : ), ∫ (x : ) in 0..t, g x) filter.at_top filter.at_top

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) :
filter.tendsto (λ (t : ), ∫ (x : ) in 0..t, g x) filter.at_bot filter.at_bot

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) :
filter.tendsto (λ (t : ), ∫ (x : ) in 0..t, g x) filter.at_top filter.at_top

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) :
filter.tendsto (λ (t : ), ∫ (x : ) in 0..t, g x) filter.at_bot filter.at_bot

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