English
Let f be in L1 with respect to μ. Then for every ε > 0 there exists a real number M ≥ 0 such that the tail of f past level M has arbitrarily small L1-norm: the integral of the tail portion of f, i.e. the function x ↦ f(x) on {x : M ≤ ∥f(x)∥_+}, and 0 elsewhere, has integral at most ε.
Русский
Пусть f ∈ L¹(μ). Тогда для каждого ε > 0 существует M ≥ 0 такое, что хвостовая часть f, начинающаяся с порога M, имеет произвольную малую L¹-норму: интеграл от хвостовой части f, то есть функция x ↦ f(x) на множестве {x : M ≤ ∥f(x)∥_+}, и 0 вне него, не превышает ε.
LaTeX
$$$\exists M \in \mathbb{R},\ 0 \le M\ \land\ \int \|\{x \mid M \le \|f(x)\|_+\}.indicator\ f(x)\|\ dμ \le ε$$$
Lean4
theorem integral_indicator_norm_ge_nonneg_le (hf : MemLp f 1 μ) {ε : ℝ} (hε : 0 < ε) :
∃ M : ℝ, 0 ≤ M ∧ (∫⁻ x, ‖{x | M ≤ ‖f x‖₊}.indicator f x‖ₑ ∂μ) ≤ ENNReal.ofReal ε :=
by
have hf_mk : MemLp (hf.1.mk f) 1 μ := (memLp_congr_ae hf.1.ae_eq_mk).mp hf
obtain ⟨M, hM_pos, hfM⟩ := hf_mk.integral_indicator_norm_ge_nonneg_le_of_meas hf.1.stronglyMeasurable_mk hε
refine ⟨M, hM_pos, (le_of_eq ?_).trans hfM⟩
refine lintegral_congr_ae ?_
filter_upwards [hf.1.ae_eq_mk] with x hx
simp only [Set.indicator_apply, coe_nnnorm, Set.mem_setOf_eq, hx.symm]
