mathlib3 documentation

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]
@[protected, measurability]
@[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]

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

noncomputable def add_circle.measurable_equiv_Ioc (T : ) [hT : fact (0 < T)] (a : ) :

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 : ) :

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 : add_circle T ennreal) :
∫⁻ (a : ) in set.Ioc t (t + T), f a = ∫⁻ (b : add_circle T), 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (t : ) (f : add_circle T E) :
(a : ) in set.Ioc t (t + T), f a = (b : add_circle T), 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} [normed_add_comm_group E] [normed_space E] [complete_space E] (t : ) (f : add_circle T E) :
(a : ) in t..t + T, f a = (b : add_circle T), 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]

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]

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]

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]

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} [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.

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.

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

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

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.

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.

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) :

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 : 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) :

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 : 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) :

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 : 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) :

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