Integral limits on large events

Bounded convergence localized to a good measurable event gives an eventual integral bound, with an explicit multiple of the measure of the complementary event.

theorem BGW.Probability.eventually_integral_le_of_tendsto_on {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.ProbabilityMeasure Ω) {e : ℕ → Ω → ℝ} {G : Set Ω} (hG : MeasurableSet G) {C : ℝ} (hC : 0 ≤ C) (he : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (e n) ↑P) (hbound : ∀ (n : ℕ), ∀ᵐ (p : Ω) ∂↑P, 0 ≤ e n p ∧ e n p ≤ C) (hconv : ∀ᵐ (p : Ω) ∂↑P, p ∈ G → Filter.Tendsto (fun (n : ℕ) => e n p) Filter.atTop (nhds 0)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (p : Ω), e n p ∂↑P < C * (↑P).real Gᶜ + ε

Full-sequence bounded convergence on a good event gives an eventual integral bound, paying only the uniform bound times the probability of its complement.