English
If f is integrable and E is a normed space, then for each y, the sum over n of ∫_{y+n}^{y+n+1} f converges to ∫ f.
Русский
Если f интегрируема и у нас есть пространство нормы, то сумма по n ∫_{y+n}^{y+n+1} f равна интегралу по всему.
LaTeX
$$$HasSum \\{\\int_{y+n}^{y+n+1} f(x)dx\\}_{n\\in\\mathbb{Z}} = \\int_{\\mathbb{R}} f(x)dx$.$$
Lean4
theorem abs_integral_mono_interval {c d} (h : Ι a b ⊆ Ι c d) (hf : 0 ≤ᵐ[μ.restrict (Ι c d)] f)
(hfi : IntervalIntegrable f μ c d) : |∫ x in a..b, f x ∂μ| ≤ |∫ x in c..d, f x ∂μ| :=
have hf' : 0 ≤ᵐ[μ.restrict (Ι a b)] f := ae_mono (Measure.restrict_mono h le_rfl) hf
calc
|∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| := abs_integral_eq_abs_integral_uIoc f
_ = ∫ x in Ι a b, f x ∂μ := (abs_of_nonneg (MeasureTheory.integral_nonneg_of_ae hf'))
_ ≤ ∫ x in Ι c d, f x ∂μ := (setIntegral_mono_set hfi.def' hf h.eventuallyLE)
_ ≤ |∫ x in Ι c d, f x ∂μ| := (le_abs_self _)
_ = |∫ x in c..d, f x ∂μ| := (abs_integral_eq_abs_integral_uIoc f).symm
