α : Type u_2
E : Type u_3
F✝ : Type ?u.995907
𝕜 : Type ?u.995910
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
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → E
f : α → E
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => if hf : Integrable fun a => F n a then ↑L1.integralCLM (Integrable.toL1 (fun a => F n a) hf) else 0)
    l (𝓝 (if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0))
α : Type u_2
E : Type u_3
F✝ : Type ?u.995907
𝕜 : Type ?u.995910
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
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → E
f : α → E
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (𝓝 (∫ (a : α), f a ∂μ))
simp only [integral, L1.integral]
no goals
α : Type u_2
E : Type u_3
F✝ : Type ?u.995907
𝕜 : Type ?u.995910
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
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → E
f : α → E
bound : α → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
bound_integrable : Integrable bound
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => if hf : Integrable fun a => F n a then ↑L1.integralCLM (Integrable.toL1 (fun a => F n a) hf) else 0)
    l (𝓝 (if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0))
exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
  bound hF_meas h_bound bound_integrable h_lim