theorem dominated_convergence_theorem {α : Type u_1} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → G} {f : α → G} {bound : α → ℝ} (hF_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) (h_bound_int : MeasureTheory.Integrable bound μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))

Dominated convergence theorem. If F n → f pointwise almost everywhere, each F n is almost-everywhere strongly measurable, and ‖F n a‖ ≤ bound a a.e. for an integrable function bound, then ∫ F n dμ → ∫ f dμ.