English
For periodic g with period T > 0, the integral from 0 to t is bounded below by a floor-term times the T-interval integral plus a fixed infimum constant.
Русский
Для периодической g с периодом T>0 интеграл от 0 до t ограничен ниже целочисленным членом, пропорциональным интегралу по [0,T], плюс константа.
LaTeX
$$$\\int_{0}^{t} g(x)dx \\ge \\inf_{u\\in[0,T]} \\int_{0}^{u} g(x)dx + \\Big\\lfloor\\frac{t}{T}\\Big\\2 \\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_atTop_intervalIntegral_of_pos (h₀ : 0 < ∫ x in 0..T, g x) (hT : 0 < T) :
Tendsto (fun t => ∫ x in 0..t, g x) atTop atTop :=
by
have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'
apply tendsto_atTop_mono (hg.sInf_add_zsmul_le_integral_of_pos h_int hT)
apply atTop.tendsto_atTop_add_const_left (sInf <| (fun t => ∫ x in 0..t, g x) '' Icc 0 T)
apply Tendsto.atTop_zsmul_const h₀
exact tendsto_floor_atTop.comp (tendsto_id.atTop_mul_const (inv_pos.mpr hT))
