English
For integrable f on [a,b], [c,d], one has a specific rearrangement identity: integral over [a,b] plus integral over [c,d] equals integral over [a,d] plus integral over [c,b].
Русский
Для интегрируемой функции на интервалах [a,b] и [c,d] выполняется тождество перераспределения интегралов: сумма интегралов по двух соседним интервалам равна сумме интегралов по перекрёстным интервалам.
LaTeX
$$$ \\int_{a}^{b} f(x) \\, dμ + \\int_{c}^{d} f(x) \\, dμ = \\int_{a}^{d} f(x) \\, dμ + \\int_{c}^{b} f(x) \\, dμ $$$
Lean4
theorem integral_interval_sub_interval_comm (hab : IntervalIntegrable f μ a b) (hcd : IntervalIntegrable f μ c d)
(hac : IntervalIntegrable f μ a c) :
((∫ x in a..b, f x ∂μ) - ∫ x in c..d, f x ∂μ) = (∫ x in a..c, f x ∂μ) - ∫ x in b..d, f x ∂μ := by
simp only [sub_eq_add_neg, ← integral_symm, integral_interval_add_interval_comm hab hcd.symm (hac.trans hcd)]