English
If μ is finite and each AEStronglyMeasurable f_i is given and there exists a C for every ε>0 such that the tail after truncation is bounded by ε, then UniformIntegrable holds for f.
Русский
При конечной мере μ и существовании C для каждого ε>0 такое, что хвост после усечения ограничен ε, то f равномерно интегрируемо.
LaTeX
$$$IsFiniteMeasure(\mu) \land (1 \le p) \land (p \neq \infty) \land (\forall i, AEStronglyMeasurable(f_i)) \land (\forall \varepsilon>0, \exists C \ge 0,\forall i,\ eLpNorm(\{x: C \le \|f_i(x)\|_+\}.indicator(f_i)) \;p\;\mu \le ENNReal.ofReal(\varepsilon)) \Rightarrow \mathrm{UniformIntegrable}(f,p,\mu)$$$
Lean4
/-- A sequence of functions `(fₙ)` is uniformly integrable in the probability sense if for all
`ε > 0`, there exists some `C` such that `∫ x in {|fₙ| ≥ C}, fₙ x ∂μ ≤ ε` for all `n`. -/
theorem uniformIntegrable_of [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ i, AEStronglyMeasurable (f i) μ)
(h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
UniformIntegrable f p μ := by
set g : ι → α → β := fun i => (hf i).choose
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hf i).1
have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hf i).2.symm
refine (uniformIntegrable_of' hp hp' hgmeas fun ε hε => ?_).ae_eq hgeq
obtain ⟨C, hC⟩ := h ε hε
refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
by_cases hfx : x ∈ {x | C ≤ ‖f i x‖₊}
· rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
rwa [Set.mem_setOf, hx] at hfx
· rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
rwa [Set.mem_setOf, hx] at hfx
