English
Equivalence between two principal formulations of uniform integrability under finite measure and p in (1,∞].
Русский
Эквивалентность двух основных формулировок равномерной интегрируемости при конечной мере и p в (1,∞].
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
theorem spec (hp : p ≠ 0) (hp' : p ≠ ∞) (hfu : UniformIntegrable f p μ) {ε : ℝ} (hε : 0 < ε) :
∃ C : ℝ≥0, ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε :=
by
set g : ι → α → β := fun i => (hfu.1 i).choose
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfu.1 i).1
have hgunif : UniformIntegrable g p μ := hfu.ae_eq fun i => (Exists.choose_spec <| hfu.1 i).2
obtain ⟨C, hC⟩ := hgunif.spec' hp hp' hgmeas hε
refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
filter_upwards [(Exists.choose_spec <| hfu.1 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
