def TheoryOfProbability3.TextbookUniformlyIntegrable {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} (f : ι → α → ℝ) (μ : MeasureTheory.Measure α) : Prop

Textbook (Durrett) definition of uniform integrability of a family of real-valued functions f : ι → α → ℝ with respect to a measure μ: each f i is AEStronglyMeasurable, and for every ε > 0 there is a uniform truncation level C : ℝ≥0 so that the tail L¹ mass ∫ |f i| · 1_{C ≤ ‖f i‖} dμ ≤ ε for every i. This matches the textbook formulation lim_{M→∞} sup_i E(|X_i|; |X_i| > M) = 0.