tendsto_atBot_intervalIntegral_of_pos'

English

Under the same hypotheses as above (g positive, periodic with period T > 0), the function t ↦ ∫_0^t g(x) dx tends to -∞ as t → -∞.

Русский

При тех же допущениях, что и выше, функция t ↦ ∫_0^t g(x) dx стремится к −∞ при 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). $$$$

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_atBot_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) atBot atBot := by
  exact hg.tendsto_atBot_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

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