English
A second auxiliary lemma analog to unifIntegrable_of' providing a constructive bound via C and ε for all i.
Русский
Вторая вспомогательная лемма аналогична unifIntegrable_of' и обеспечивает конструктивную границу через C и ε.
LaTeX
$$$\text{unifIntegrable_of'}(hp, hp', f, h)$$$
Lean4
theorem unifIntegrable_of (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β} (hf : ∀ i, AEStronglyMeasurable (f i) μ)
(h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) :
UnifIntegrable f p μ := by
set g : ι → α → β := fun i => (hf i).choose
refine
(unifIntegrable_of' hp hp' (fun i => (Exists.choose_spec <| hf i).1) fun ε hε => ?_).ae_eq fun i =>
(Exists.choose_spec <| hf i).2.symm
obtain ⟨C, hC⟩ := h ε hε
have hCg : ∀ i, eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε :=
by
intro i
refine 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
refine ⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (eLpNorm_mono fun x => ?_) (hCg i)⟩
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
exact
Set.indicator_le_indicator_of_subset (fun x hx => Set.mem_setOf_eq ▸ le_trans (le_max_left _ _) hx)
(fun _ => norm_nonneg _) _
