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.

source

theorem is_add_fundamental_domain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : measure_theory.measure ℝ . "volume_tac") :

measure_theory.is_add_fundamental_domain ↥(add_subgroup.zmultiples T) (set.Ioc t (t + T)) μ

source

theorem function.periodic.interval_integral_add_eq_of_pos {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : ℝ → E} {T : ℝ} (hf : function.periodic f 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.

source

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

source

theorem function.periodic.interval_integral_add_eq_add {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : ℝ → E} {T : ℝ} (hf : function.periodic f T) (t s : ℝ) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable f measure_theory.measure_space.volume 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].

source

theorem function.periodic.interval_integral_add_zsmul_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : ℝ → E} {T : ℝ} (hf : function.periodic f T) (n : ℤ) (t : ℝ) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable f measure_theory.measure_space.volume 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].

source

theorem function.periodic.Inf_add_zsmul_le_integral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume t₁ t₂) (hT : 0 < T) (t : ℝ) :

has_Inf.Inf ((λ (t : ℝ), ∫ (x : ℝ) in 0..t, g x) '' set.Icc 0 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.

source

theorem function.periodic.integral_le_Sup_add_zsmul_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume t₁ t₂) (hT : 0 < T) (t : ℝ) :

∫ (x : ℝ) in 0..t, g x ≤ has_Sup.Sup ((λ (t : ℝ), ∫ (x : ℝ) in 0..t, g x) '' set.Icc 0 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.

source

theorem function.periodic.tendsto_at_top_interval_integral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume 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 ∞.

source

theorem function.periodic.tendsto_at_bot_interval_integral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume 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 -∞.

source

theorem function.periodic.tendsto_at_top_interval_integral_of_pos' {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume 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 ∞.

source

theorem function.periodic.tendsto_at_bot_interval_integral_of_pos' {T : ℝ} {g : ℝ → ℝ} (hg : function.periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), interval_integrable g measure_theory.measure_space.volume 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 -∞.