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

Textbook definition of uniform integrability of a family f : ι → α → ℝ: each f i is AEStronglyMeasurable and for every ε > 0 there is a uniform truncation level C : ℝ≥0 such that the L¹ norm of the tail {x | C ≤ ‖f i x‖₊}.indicator (f i) is at most ε for all i. This matches Durrett's definition: lim_{M→∞} sup_i E(|X_i|; |X_i| > M) = 0.

theorem TheoryOfProbability3.textbookUI'_iff_uniformIntegrable {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (f : ι → α → ℝ) : TextbookUniformlyIntegrable' f μ ↔ MeasureTheory.UniformIntegrable f 1 μ

On a finite measure space, the textbook definition TextbookUniformlyIntegrable' is equivalent to Mathlib's UniformIntegrable f 1 μ.

@[reducible, inline]

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

Uniform absolute continuity of the L¹ integrals of a family f : ι → α → ℝ, expressed via Mathlib's UnifIntegrable f 1 μ.

@[reducible, inline]

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

A uniform L¹-bound on the family f : ι → α → ℝ: there exists C : ℝ≥0 with ‖f i‖₁ ≤ C for all i.

theorem TheoryOfProbability3.textbookUI_iff_bound_and_unifAbsCont {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (f : ι → α → ℝ) : TextbookUniformlyIntegrable' f μ ↔ (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) ∧ UnifAbsContIntegrals f μ ∧ UnifL1Bound f μ

On a finite measure space, the textbook notion of uniform integrability is equivalent to the conjunction of: (i) each f i is AEStronglyMeasurable, (ii) uniform absolute continuity of integrals, and (iii) a uniform L¹-bound.

theorem TheoryOfProbability3.TextbookUniformlyIntegrable'.unifL1Bound {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : ι → α → ℝ} (hf : TextbookUniformlyIntegrable' f μ) : UnifL1Bound f μ

A uniformly integrable family (in the textbook sense) is uniformly bounded in L¹.

theorem TheoryOfProbability3.TextbookUniformlyIntegrable'.unifAbsContIntegrals {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : ι → α → ℝ} (hf : TextbookUniformlyIntegrable' f μ) : UnifAbsContIntegrals f μ

A uniformly integrable family (in the textbook sense) has uniformly absolutely continuous integrals.

theorem TheoryOfProbability3.TextbookUniformlyIntegrable'.aEStronglyMeasurable' {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : ι → α → ℝ} (hf : TextbookUniformlyIntegrable' f μ) (i : ι) : MeasureTheory.AEStronglyMeasurable (f i) μ

Each function in a uniformly integrable family is AEStronglyMeasurable.