English
For a periodic g with period T > 0, the lower envelope of cumulative interval integrals grows at least like X + floor(t/T)Y for appropriate constants X,Y.
Русский
Для периодической g с T>0 нижняя грань суммарных интегралов растет не ниже X + ⌊t/T⌋Y на подходящих константах X,Y.
LaTeX
$$$sInf(\\{\\int_0^t g(x)dx: t\\in[0,T]\\}) + \\lfloor t/T \\rfloor \\cdot \\int_0^T g(x)dx \\le \\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 below by `t ↦ X + ⌊t/T⌋ • Y` for appropriate constants `X` and
`Y`. -/
theorem sInf_add_zsmul_le_integral_of_pos (h_int : IntervalIntegrable g MeasureSpace.volume 0 T) (hT : 0 < T) (t : ℝ) :
(sInf ((fun t => ∫ x in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ x in 0..T, g x) ≤ ∫ x in 0..t, g x :=
by
let h'_int := hg.intervalIntegrable₀ hT h_int
let ε := Int.fract (t / T) * T
conv_rhs =>
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⌋ ε (hg.intervalIntegrable₀ hT h_int), hg.intervalIntegral_add_eq ε 0,
zero_add, add_le_add_iff_right]
exact
(continuous_primitive h'_int 0).continuousOn.sInf_image_Icc_le <|
mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT)
