Integrals of periodic functions

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 AddCircle.measurePreserving_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.intervalIntegral_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.

theorem AddCircle.measurable_mk' {a : ℝ} : Measurable QuotientAddGroup.mk

theorem isAddFundamentalDomain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : MeasureTheory.Measure ℝ := by volume_tac) : MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T)) (Set.Ioc t (t + T)) μ

theorem isAddFundamentalDomain_Ioc' {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : MeasureTheory.Measure ℝ := by volume_tac) : MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T).op) (Set.Ioc t (t + T)) μ

noncomputable instance AddCircle.measureSpace (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.MeasureSpace (AddCircle T)

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

Equations

• AddCircle.measureSpace T = MeasureTheory.MeasureSpace.mk (ENNReal.ofReal T • MeasureTheory.Measure.addHaarMeasure ⊤)

@[simp]

theorem AddCircle.measure_univ (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.volume Set.univ = ENNReal.ofReal T

instance AddCircle.instIsAddHaarMeasureRealVolume (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.volume.IsAddHaarMeasure

instance AddCircle.isFiniteMeasure (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.IsFiniteMeasure MeasureTheory.volume

instance AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.HasAddFundamentalDomain ↥(AddSubgroup.zmultiples T).op ℝ MeasureTheory.volume

instance AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.AddQuotientMeasureEqMeasurePreimage MeasureTheory.volume MeasureTheory.volume

theorem AddCircle.measurePreserving_mk (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) : MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + T))) MeasureTheory.volume

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 AddCircle.add_projection_respects_measure (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) {U : Set (AddCircle T)} (meas_U : MeasurableSet U) : MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ioc t (t + T))

theorem AddCircle.volume_closedBall (T : ℝ) [hT : Fact (0 < T)] {x : AddCircle T} (ε : ℝ) : MeasureTheory.volume (Metric.closedBall x ε) = ENNReal.ofReal (T ⊓ 2 * ε)

instance AddCircle.instIsUnifLocDoublingMeasureRealVolume (T : ℝ) [hT : Fact (0 < T)] : IsUnifLocDoublingMeasure MeasureTheory.volume

noncomputable def AddCircle.measurableEquivIoc (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ioc a (a + T))

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

Equations

• AddCircle.measurableEquivIoc T a = { toEquiv := AddCircle.equivIoc T a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

noncomputable def AddCircle.measurableEquivIco (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ico a (a + T))

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

Equations

• AddCircle.measurableEquivIco T a = { toEquiv := AddCircle.equivIco T a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem AddCircle.lintegral_preimage (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) (f : AddCircle T → ENNReal) : ∫⁻ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b

The lower integral of a function over AddCircle T is equal to the lower integral over an interval (t, t + T] in ℝ of its lift to ℝ.

theorem AddCircle.integral_preimage (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : AddCircle T → E) : ∫ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

The integral of an almost-everywhere strongly measurable function over AddCircle T is equal to the integral over an interval (t, t + T] in ℝ of its lift to ℝ.

theorem AddCircle.intervalIntegral_preimage (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : AddCircle T → E) : ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b

The integral of an almost-everywhere strongly measurable function over AddCircle T is equal to the integral over an interval (t, t + T] in ℝ of its lift to ℝ.

theorem UnitAddCircle.measure_univ : MeasureTheory.volume Set.univ = 1

theorem UnitAddCircle.measurePreserving_mk (t : ℝ) : MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + 1))) MeasureTheory.volume

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

theorem UnitAddCircle.lintegral_preimage (t : ℝ) (f : UnitAddCircle → ENNReal) : ∫⁻ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫⁻ (b : UnitAddCircle), f b

The integral of a measurable function over UnitAddCircle is equal to the integral over an interval (t, t + 1] in ℝ of its lift to ℝ.

theorem UnitAddCircle.integral_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E) : ∫ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫ (b : UnitAddCircle), f b

The integral of an almost-everywhere strongly measurable function over UnitAddCircle is equal to the integral over an interval (t, t + 1] in ℝ of its lift to ℝ.

theorem UnitAddCircle.intervalIntegral_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E) : ∫ (a : ℝ) in t..t + 1, f ↑a = ∫ (b : UnitAddCircle), f b

The integral of an almost-everywhere strongly measurable function over UnitAddCircle is equal to the integral over an interval (t, t + 1] in ℝ of its lift to ℝ.

theorem Function.Periodic.intervalIntegral_add_eq_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ 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.intervalIntegral_add_eq.

theorem Function.Periodic.intervalIntegral_add_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ 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.intervalIntegral_add_eq_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {T : ℝ} (hf : Function.Periodic f T) (t s : ℝ) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.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.intervalIntegral_add_zsmul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {T : ℝ} (hf : Function.Periodic f T) (n : ℤ) (t : ℝ) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.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.sInf_add_zsmul_le_integral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (hT : 0 < T) (t : ℝ) : sInf ((fun (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_sSup_add_zsmul_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (hT : 0 < T) (t : ℝ) : ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun (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_atTop_intervalIntegral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x) (hT : 0 < T) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop

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_atBot_intervalIntegral_of_pos {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x) (hT : 0 < T) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot

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_atTop_intervalIntegral_of_pos' {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (h₀ : ∀ (x : ℝ), 0 < g x) (hT : 0 < T) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop

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_atBot_intervalIntegral_of_pos' {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) (h₀ : ∀ (x : ℝ), 0 < g x) (hT : 0 < T) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot

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