α : Type u_2
β : Type ?u.62254
E : Type u_3
F : Type ?u.62260
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
hfi : Integrable f
⊢ HasSum (fun n => ∫ (a : α) in s n, f a ∂μ) (∫ (a : α), f a ∂Measure.sum fun i => Measure.restrict μ (s i))
α : Type u_2
β : Type ?u.62254
E : Type u_3
F : Type ?u.62260
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ (i : ι), s i)
⊢ HasSum (fun n => ∫ (a : α) in s n, f a ∂μ) (∫ (a : α) in ⋃ (n : ι), s n, f a ∂μ)
simp only [IntegrableOn, Measure.restrict_iUnion_ae hd hm] at hfi ⊢
no goals
α : Type u_2
β : Type ?u.62254
E : Type u_3
F : Type ?u.62260
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
hfi : Integrable f
⊢ HasSum (fun n => ∫ (a : α) in s n, f a ∂μ) (∫ (a : α), f a ∂Measure.sum fun i => Measure.restrict μ (s i))
exact hasSum_integral_measure hfi