ι : Type ?u.21798231
𝕜 : Type ?u.21798234
E : Type u_1
F : Type ?u.21798240
A : Type ?u.21798243
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
ι : Type ?u.21798231
𝕜 : Type ?u.21798234
E : Type u_1
F : Type ?u.21798240
A : Type ?u.21798243
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
simp_rw [integral_of_le (le_add_of_nonneg_right zero_le_one)]
ι : Type ?u.21798231
𝕜 : Type ?u.21798234
E : Type u_1
F : Type ?u.21798240
A : Type ?u.21798243
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)
    (∫ (x : ℝ) in ⋃ (n : ℤ), Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)
ι : Type ?u.21798231
𝕜 : Type ?u.21798234
E : Type u_1
F : Type ?u.21798240
A : Type ?u.21798243
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
rw [← integral_univ, ← iUnion_Ioc_add_int_cast y]
no goals
ι : Type ?u.21798231
𝕜 : Type ?u.21798234
E : Type u_1
F : Type ?u.21798240
A : Type ?u.21798243
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)
    (∫ (x : ℝ) in ⋃ (n : ℤ), Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)
exact
  hasSum_integral_iUnion (fun i => measurableSet_Ioc) (pairwise_disjoint_Ioc_add_int_cast y)
    hfi.integrableOn