integral_add_adjacent_intervals_cancel

English

If f is interval-integrable on a,b and b,c, then the triple sum (∫_a^b f + ∫_b^c f + ∫_c^a f) equals zero.

Русский

Пусть f интегрируема по интервалам a,b и b,c; тогда сумма трех соответствующих интегралов равна нулю.

LaTeX

$$$( \\int_{a}^{b} f(x) \\, dμ ) + ( \\int_{b}^{c} f(x) \\, dμ ) + ( \\int_{c}^{a} f(x) \\, dμ ) = 0$$

Lean4

theorem integral_add_adjacent_intervals_cancel (hab : IntervalIntegrable f μ a b) (hbc : IntervalIntegrable f μ b c) :
    (((∫ x in a..b, f x ∂μ) + ∫ x in b..c, f x ∂μ) + ∫ x in c..a, f x ∂μ) = 0 :=
  by
  have hac := hab.trans hbc
  simp only [intervalIntegral, sub_add_sub_comm, sub_eq_zero]
  iterate 4 rw [← setIntegral_union]
  · suffices Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c by rw [this]
    rw [Ioc_union_Ioc_union_Ioc_cycle, union_right_comm, Ioc_union_Ioc_union_Ioc_cycle, min_left_comm, max_left_comm]
  all_goals simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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