English
If μ has finite measure and each f_i is AEStronglyMeasurable, and for every ε>0 there exists C such that the tail after truncation has L^p-norm ≤ ε for all i, then UniformIntegrable holds.
Русский
При конечной мере μ и AEStronglyMeasurable f_i, если для каждого ε>0 существует C, так что хвост после усечения имеет p-норму ≤ ε для всех i, то выполняется UniformIntegrable.
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
/-- This lemma is superseded by `uniformIntegrable_of` which only requires
`AEStronglyMeasurable`. -/
theorem uniformIntegrable_of' [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ i, StronglyMeasurable (f i))
(h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
UniformIntegrable f p μ :=
by
refine ⟨fun i => (hf i).aestronglyMeasurable, unifIntegrable_of hp hp' (fun i => (hf i).aestronglyMeasurable) h, ?_⟩
obtain ⟨C, hC⟩ := h 1 one_pos
refine ⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).toNNReal, fun i => ?_⟩
calc
eLpNorm (f i) p μ ≤
eLpNorm ({x : α | ‖f i x‖₊ < C}.indicator (f i)) p μ + eLpNorm ({x : α | C ≤ ‖f i x‖₊}.indicator (f i)) p μ :=
by
refine
le_trans (eLpNorm_mono_enorm fun x => ?_)
(eLpNorm_add_le
(StronglyMeasurable.aestronglyMeasurable
((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
(StronglyMeasurable.aestronglyMeasurable
((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm)))
hp)
rw [Pi.add_apply, Set.indicator_apply]
split_ifs with hx
· rw [Set.indicator_of_notMem, add_zero]
simpa using hx
· rw [Set.indicator_of_mem, zero_add]
simpa using hx
_ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 :=
by
have : ∀ᵐ x ∂μ, ‖{x : α | ‖f i x‖₊ < C}.indicator (f i) x‖₊ ≤ C :=
by
filter_upwards
simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
exact Set.indicator_le fun x (hx : _ < _) => hx.le
refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
exact le_rfl
_ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by rw [ENNReal.coe_toNNReal (by finiteness)]
