Theorems · Theorem · measure theory

Function.Periodic.tendsto_atTop_intervalIntegral_of_pos

∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    0 < ∫ (x : ℝ) in 0..T, g x → 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 ∞.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Cited by

1 results in Mathlib

Foundations

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