α : Type u_3
E : Type u_2
F : Type ?u.898484
𝕜 : Type ?u.898487
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ (if hf : Integrable fun a => ∑ i in s, f i a then ↑L1.integralCLM (Integrable.toL1 (fun a => ∑ i in s, f i a) hf)
    else 0) =
    ∑ x in s, if hf : Integrable fun a => f x a then ↑L1.integralCLM (Integrable.toL1 (fun a => f x a) hf) else 0
α : Type u_3
E : Type u_2
F : Type ?u.898484
𝕜 : Type ?u.898487
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ (∫ (a : α), ∑ i in s, f i a ∂μ) = ∑ i in s, ∫ (a : α), f i a ∂μ
simp only [integral, L1.integral]
no goals
α : Type u_3
E : Type u_2
F : Type ?u.898484
𝕜 : Type ?u.898487
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ (if hf : Integrable fun a => ∑ i in s, f i a then ↑L1.integralCLM (Integrable.toL1 (fun a => ∑ i in s, f i a) hf)
    else 0) =
    ∑ x in s, if hf : Integrable fun a => f x a then ↑L1.integralCLM (Integrable.toL1 (fun a => f x a) hf) else 0
exact setToFun_finset_sum (dominatedFinMeasAdditive_weightedSMul _) s hf