integral_interval_sub_interval_comm

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)]

Похожие утверждения