Documentation

Mathlib.MeasureTheory.Integral.Periodic

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
noncomputable instance AddCircle.measureSpace (T : ) [hT : Fact (0 < T)] :

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

Equations
@[simp]
theorem AddCircle.measure_univ (T : ) [hT : Fact (0 < T)] :
MeasureTheory.volume Set.univ = ENNReal.ofReal T
instance AddCircle.isFiniteMeasure (T : ) [hT : Fact (0 < T)] :
MeasureTheory.IsFiniteMeasure MeasureTheory.volume
Equations
  • =
theorem AddCircle.measurePreserving_mk (T : ) [hT : Fact (0 < T)] (t : ) :
MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.Measure.restrict MeasureTheory.volume (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.volume_closedBall (T : ) [hT : Fact (0 < T)] {x : AddCircle T} (ε : ) :
MeasureTheory.volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
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
Instances For
    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
    Instances For
      theorem AddCircle.lintegral_preimage (T : ) [hT : Fact (0 < T)] (t : ) (f : AddCircle TENNReal) :
      ∫⁻ (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 TE) :
      ∫ (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 TE) :
      ∫ (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.Measure.restrict MeasureTheory.volume (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 : UnitAddCircleENNReal) :
      ∫⁻ (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 : UnitAddCircleE) :
      ∫ (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 : UnitAddCircleE) :
      ∫ (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 -∞.