theorem DominatedConvergence.dominated_convergence_integrable_and_tendsto {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → ℝ} {f g : α → ℝ} (hF_integrable : ∀ (n : ℕ), MeasureTheory.Integrable (F n) μ) (hg_integrable : MeasureTheory.Integrable g μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ g a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : MeasureTheory.Integrable f μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))

Dominated Convergence Theorem (Melrose Theorem 4.6): if (Fₙ) is integrable, dominated by an integrable g, and converges pointwise a.e. to f, then f is integrable and the integrals of Fₙ converge to the integral of f.