∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      (∀ (x : ℝ), 0 < g x) → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atTop Filter.atTop