English
For a natural index sequence a: N → R and m ≤ n, under suitable interval integrability, the sum of ∫ a(k) to a(k+1) equals ∫ a(m) to a(n).
Русский
Для последовательности a(k) вещественных чисел при условии интервальной интегрируемости сумма интегралов по соседним интервалам равна интегралу по суммарному интервалу.
LaTeX
$$$ \\sum_{k=m}^{n-1} \\int_{a(k)}^{a(k+1)} f(x) \\, dμ = \\int_{a(m)}^{a(n)} f(x) \\, dμ $$$
Lean4
theorem sum_integral_adjacent_intervals_Ico {a : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n)
(hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a <| k + 1)) :
∑ k ∈ Finset.Ico m n, ∫ x in a k..a <| k + 1, f x ∂μ = ∫ x in a m..a n, f x ∂μ :=
by
revert hint
refine Nat.le_induction ?_ ?_ n hmn
· simp
· intro p hmp IH h
rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
· refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_
exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk
· apply h
simp [hmp]
· intro k hk
exact h _ (Ico_subset_Ico_right p.le_succ hk)
