α : Type u_3
E : Type u_2
F✝ : Type ?u.983342
𝕜 : Type ?u.983345
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
f : α → E
hfi : Integrable f
F : ι → α → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i)
hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => if hf : Integrable fun x => F i x then ↑L1.integralCLM (Integrable.toL1 (fun x => F i x) hf) else 0)
    l (𝓝 (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0))
α : Type u_3
E : Type u_2
F✝ : Type ?u.983342
𝕜 : Type ?u.983345
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
f : α → E
hfi : Integrable f
F : ι → α → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i)
hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
simp only [integral, L1.integral]
no goals
α : Type u_3
E : Type u_2
F✝ : Type ?u.983342
𝕜 : Type ?u.983345
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
f : α → E
hfi : Integrable f
F : ι → α → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i)
hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => if hf : Integrable fun x => F i x then ↑L1.integralCLM (Integrable.toL1 (fun x => F i x) hf) else 0)
    l (𝓝 (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0))
exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF