tendsto_atTop_intervalIntegral_of_pos'

English

Let g: R → R be a positive-valued function that is periodic with period T > 0. Then the function t ↦ ∫ from 0 to t g(x) dx grows without bound as t → ∞; in particular, it tends to +∞.

Русский

Пусть g: ℝ → ℝ является неотрицательной периодической с периодом T > 0 и g(x) > 0 для всех x. Тогда функция t ↦ ∫_0^t g(x) dx растет бесконечно быстро, то есть tends к +∞ при t → ∞.

LaTeX

$$$$ \\lim_{t \\to \\infty} \\int_{0}^{t} g(x)\\,dx = \\infty \\quad\\text{(with } g \\text{ periodic of period } T>0,\\; g(x)>0\\text{ for all }x). $$$$

Lean4

/-- 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 tendsto_atTop_intervalIntegral_of_pos' (h_int : IntervalIntegrable g MeasureSpace.volume 0 T)
    (h₀ : ∀ x, 0 < g x) (hT : 0 < T) : Tendsto (fun t => ∫ x in 0..t, g x) atTop atTop :=
  hg.tendsto_atTop_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

Похожие утверждения