Theorems · Theorem · measure theory

Function.Periodic.integral_le_sSup_add_zsmul_of_pos

∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      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.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

1 results in Mathlib

Foundations

Depth 263 from the axioms · uses propext, Classical.choice, Quot.sound