integral_Iic_sub_Iic — Mathlib

English

The difference of integrals over Iic(b) and Iic(a) equals the integral over [a,b].

Русский

Разность интегралов по множестваам Iic(b) и Iic(a) равна интегралу по интервалу [a,b].

LaTeX

$$$ \\int_{Iic(b)} f \\, dμ - \\int_{Iic(a)} f \\, dμ = \\int_{a}^{b} f(x) \\, dμ $$$

Lean4

theorem integral_Iic_sub_Iic (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) :
    ((∫ x in Iic b, f x ∂μ) - ∫ x in Iic a, f x ∂μ) = ∫ x in a..b, f x ∂μ :=
  by
  wlog hab : a ≤ b generalizing a b
  · rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]
  rw [sub_eq_iff_eq_add', integral_of_le hab, ← setIntegral_union (Iic_disjoint_Ioc le_rfl), Iic_union_Ioc_eq_Iic hab]
  exacts [measurableSet_Ioc, ha, hb.mono_set fun _ => And.right]

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