English
The definition of uniform integrability is equivalent to the tail-control formulation stated above.
Русский
Определение равномерной интегрируемости эквивалентно формулировке по хвостам.
LaTeX
$$$\mathrm{UniformIntegrable}(f,p,\mu) \iff (\forall i, AEStronglyMeasurable(f_i)\mu) \land (\forall \varepsilon>0, \exists C≥0, \forall i, eLpNorm(...) ≤ ENNReal.ofReal(\varepsilon))$$$
Lean4
/-- The definition of uniform integrable in mathlib is equivalent to the definition commonly
found in literature. -/
theorem uniformIntegrable_iff [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) :
UniformIntegrable f p μ ↔
(∀ i, AEStronglyMeasurable (f i) μ) ∧
∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε :=
⟨fun h => ⟨h.1, fun _ => h.spec (lt_of_lt_of_le zero_lt_one hp).ne.symm hp'⟩, fun h =>
uniformIntegrable_of hp hp' h.1 h.2⟩
