ι : Type ?u.15613852
𝕜 : Type ?u.15613855
E : Type u_1
F : Type ?u.15613861
A : Type ?u.15613864
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ (k : ℕ), k < n → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
ι : Type ?u.15613852
𝕜 : Type ?u.15613855
E : Type u_1
F : Type ?u.15613861
A : Type ?u.15613864
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ (k : ℕ), k < n → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
rw [← Nat.Ico_zero_eq_range]
no goals
ι : Type ?u.15613852
𝕜 : Type ?u.15613855
E : Type u_1
F : Type ?u.15613861
A : Type ?u.15613864
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ (k : ℕ), k < n → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ (∑ k in Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
exact sum_integral_adjacent_intervals_Ico (zero_le n) fun k hk => hint k hk.2