English
Assume MemLp f with p finite and nonzero, and f is strongly measurable. If ∥f(x)∥ is bounded by M for all x, then there is δ>0 such that for every measurable set s with μ(s) ≤ δ we have eLpNorm( s.indicator f ) ≤ ε, i.e. the truncated norm is small on small sets.
Русский
Пусть f ∈ MemLp(f, p, μ) с конечным p, f измерима. Если ∥f(x)∥ ≤ M для всех x, существует δ>0, такое что для любого измеримого множества s, с μ(s) ≤ δ, выполняется eLpNorm( s.indicator f ) ≤ ε.
LaTeX
$$$\exists δ>0,\ ∀ s,\ MeasurableSet s,\ μ(s) ≤ ENNReal.ofReal δ \Rightarrow eLpNorm( s.indicator f) p μ ≤ ENNReal.ofReal ε$$$
Lean4
/-- This lemma implies that a single function is uniformly integrable (in the probability sense). -/
theorem eLpNorm_indicator_norm_ge_pos_le (hf : MemLp f p μ) (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
∃ M : ℝ, 0 < M ∧ eLpNorm ({x | M ≤ ‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε :=
by
obtain ⟨M, hM⟩ := hf.eLpNorm_indicator_norm_ge_le hmeas hε
refine ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), le_trans (eLpNorm_mono fun x => ?_) hM⟩
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
refine Set.indicator_le_indicator_of_subset (fun x hx => ?_) (fun x => norm_nonneg (f x)) x
rw [Set.mem_setOf_eq] at hx
exact (max_le_iff.1 hx).1
