English
For periodic g with period T > 0, the integral from 0 to t is bounded above by a sum of a supremum over t in [0,T] plus a floor-term times the T-interval integral.
Русский
Для периодической g с периодом T > 0 интеграл от 0 до t ограничен сверху суммой супремума по [0,T] плюс целочисленный фрагмент, умноженный на интеграл по [0,T].
LaTeX
$$$\\int_{0}^{t} g(x)dx \\le \\sup_{u\\in[0,T]} \\int_{0}^{u} g(x)dx + \\Big\\lfloor\\frac{t}{T}\\Big\\rfloor \\int_{0}^{T} g(x)dx$$$
Lean4
/-- If `g : ℝ → ℝ` is periodic with period `T > 0`, then for any `t : ℝ`, the function
`t ↦ ∫ x in 0..t, g x` is bounded above by `t ↦ X + ⌊t/T⌋ • Y` for appropriate constants `X` and
`Y`. -/
theorem integral_le_sSup_add_zsmul_of_pos (h_int : IntervalIntegrable g MeasureSpace.volume 0 T) (hT : 0 < T) (t : ℝ) :
(∫ x in 0..t, g x) ≤ sSup ((fun t => ∫ x in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ x in 0..T, g x :=
by
let h'_int := hg.intervalIntegrable₀ hT h_int
let ε := Int.fract (t / T) * T
conv_lhs =>
rw [← Int.fract_div_mul_self_add_zsmul_eq T t (by linarith), ←
integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]
rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add, add_le_add_iff_right]
exact
(continuous_primitive h'_int 0).continuousOn.le_sSup_image_Icc
(mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT))
