English
If g is periodic with period T > 0 and the integral over one period is positive, then the integral from 0 to t tends to +∞ as t → +∞.
Русский
Если g периодична и интеграл по периоду положителен, то интеграл от 0 до t стремится к +∞ при t→+∞.
LaTeX
$$$\\lim_{t\\to\\infty} \\int_{0}^{t} g(x)dx = +\\infty$ for 0 < T and 0 < \\int_{0}^{T} g(x)dx$$
Lean4
/-- 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 `-∞`. -/
theorem tendsto_atBot_intervalIntegral_of_pos (h₀ : 0 < ∫ x in 0..T, g x) (hT : 0 < T) :
Tendsto (fun t => ∫ x in 0..t, g x) atBot atBot :=
by
have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'
apply tendsto_atBot_mono (hg.integral_le_sSup_add_zsmul_of_pos h_int hT)
apply atBot.tendsto_atBot_add_const_left (sSup <| (fun t => ∫ x in 0..t, g x) '' Icc 0 T)
apply Tendsto.atBot_zsmul_const h₀
exact tendsto_floor_atBot.comp (tendsto_id.atBot_mul_const (inv_pos.mpr hT))
