English
If f is in MemLp with p = ∞, and f is strongly measurable, then there exists a threshold M such that the essential supremum of the tail part {x : M ≤ ∥f(x)∥_+}.indicator f is zero; equivalently, the tail contribution vanishes almost everywhere.
Русский
Пусть f ∈ MemLp(f, ∞, μ) и f сильно измерима. Тогда существует порог M, при котором ess sup хвостовой части {x : M ≤ ∥f(x)∥_+}.indicator f равен нулю; то есть хвост в значительной мере не вносит вклад почти нигде.
LaTeX
$$$\exists M:\mathbb{R},\ eLpNormEssSup({x:\, M \le \|f(x)\|_+}.indicator f)\, μ = 0$$$
Lean4
theorem eLpNormEssSup_indicator_norm_ge_eq_zero (hf : MemLp f ∞ μ) (hmeas : StronglyMeasurable f) :
∃ M : ℝ, eLpNormEssSup ({x | M ≤ ‖f x‖₊}.indicator f) μ = 0 :=
by
have hbdd : eLpNormEssSup f μ < ∞ := hf.eLpNorm_lt_top
refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩
rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]
· have : μ.restrict {x : α | (eLpNorm f ⊤ μ + 1).toReal ≤ ‖f x‖₊} = 0 :=
by
simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]
have : {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x : α | eLpNormEssSup f μ < ‖f x‖₊} :=
by
intro x hx
rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne, ENNReal.coe_toReal, coe_nnnorm]
refine lt_of_lt_of_le ?_ hx
rw [ENNReal.toReal_lt_toReal hbdd.ne]
· exact ENNReal.lt_add_right hbdd.ne one_ne_zero
· finiteness
rw [← nonpos_iff_eq_zero]
refine (measure_mono this).trans ?_
have hle := enorm_ae_le_eLpNormEssSup f μ
simp_rw [ae_iff, not_le] at hle
exact nonpos_iff_eq_zero.2 hle
rw [this, eLpNormEssSup_measure_zero]
exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe
