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

Bounded convergence theorem. Let μ be a probability measure and let Fₙ be a sequence of (a.e. strongly) measurable functions into a normed space with ‖Fₙ‖ ≤ C almost surely. If Fₙ → f in measure (i.e. in probability), then ∫ Fₙ dμ → ∫ f dμ.