sum_integral_adjacent_intervals — Mathlib

English

If f is interval-integrable on a sequence a(k) for k < n, then the finite sum of adjacent interval integrals equals the integral over a(0) to a(n).

Русский

Если f интегрируема по последовательности интервалов, то сумма соседних интегралов равна интегралу по началу и концу последовательности.

LaTeX

$$$ \\sum_{k=0}^{n-1} \\int_{a(k)}^{a(k+1)} f(x) \\, dμ = \\int_{a(0)}^{a(n)} f(x) \\, dμ $$$

Lean4

theorem sum_integral_adjacent_intervals {a : ℕ → ℝ} {n : ℕ}
    (hint : ∀ k < n, IntervalIntegrable f μ (a k) (a <| k + 1)) :
    ∑ k ∈ Finset.range n, ∫ x in a k..a <| k + 1, f x ∂μ = ∫ x in (a 0)..(a n), f x ∂μ :=
  by
  rw [← Nat.Ico_zero_eq_range]
  exact sum_integral_adjacent_intervals_Ico (zero_le n) fun k hk => hint k hk.2

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