α : Type u_1
E : Type u_2
F✝ : Type ?u.989419
𝕜 : Type ?u.989422
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 α
F : ℕ → α → E
f : α → E
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (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)
    atTop (𝓝 (if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0))
α : Type u_1
E : Type u_2
F✝ : Type ?u.989419
𝕜 : Type ?u.989422
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 α
F : ℕ → α → E
f : α → E
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n => ∫ (a : α), F n a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))
simp only [integral, L1.integral]
no goals
α : Type u_1
E : Type u_2
F✝ : Type ?u.989419
𝕜 : Type ?u.989422
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 α
F : ℕ → α → E
f : α → E
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (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)
    atTop (𝓝 (if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0))
exact tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
  bound F_measurable bound_integrable h_bound h_lim