English
A sequence of identically distributed Lp-valued functions is p-uniformly integrable under suitable conditions.
Русский
Последовательность идентично распределённых функций в Lp является p-однородно интегрируемой при подходящих условиях.
LaTeX
$$$hp : 1 \le p \quad \text{and} \ p ≠ ∞ \quad hℒp : MemLp (f j) p μ \quad hf : ∀ i, IdentDistrib (f i) (f j) μ μ \Rightarrow UniformIntegrable f p μ$$
Lean4
/-- A sequence of identically distributed Lᵖ functions is p-uniformly integrable. -/
theorem uniformIntegrable_of_identDistrib {ι : Type*} {f : ι → α → E} {j : ι} {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞)
(hℒp : MemLp (f j) p μ) (hf : ∀ i, IdentDistrib (f i) (f j) μ μ) : UniformIntegrable f p μ :=
by
have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i => (hf i).aestronglyMeasurable_iff.2 hℒp.1
set g : ι → α → E := fun i => (hfmeas i).choose
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfmeas i).1
have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hfmeas i).2.symm
have hgℒp : MemLp (g j) p μ := hℒp.ae_eq (hgeq j).symm
exact
UniformIntegrable.ae_eq
(MemLp.uniformIntegrable_of_identDistrib_aux hp hp' hgℒp hgmeas fun i =>
(IdentDistrib.of_ae_eq (hgmeas i).aemeasurable (hgeq i)).trans
((hf i).trans <| IdentDistrib.of_ae_eq (hfmeas j).aemeasurable (hgeq j).symm))
hgeq
