English
If f ∈ MemLp with p ≠ 0, ∞, then there exists a measurable set s with finite measure such that eLpNorm of the indicator-complemented function is small.
Русский
Если f ∈ MemLp и p ≠ 0, ∞, то существует измеримое множество s с конечной мерой, для которого eLpNorm(sᶜ.indicator f) можно сделать маленьким.
LaTeX
$$$$\\exists s \\text{ measurable}, μ(s) < ∞ \\land eLpNorm(s^c.indicator(f))_{p} < ε.$$$$
Lean4
/-- A single function that is `MemLp f p μ` is tight with respect to `μ`. -/
theorem exists_eLpNorm_indicator_compl_lt {β : Type*} [NormedAddCommGroup β] (hp_top : p ≠ ∞) {f : α → β}
(hf : MemLp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ s : Set α, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε :=
by
rcases eq_or_ne p 0 with rfl | hp₀
· use ∅;
simp [pos_iff_ne_zero.2 hε] -- first take care of `p = 0`
· obtain ⟨s, hsm, hs, hε⟩ : ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, (‖f a‖ₑ) ^ p.toReal ∂μ < ε ^ p.toReal :=
by
apply exists_setLIntegral_compl_lt
· exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne
· simp [*]
refine ⟨s, hsm, hs, ?_⟩
rwa [eLpNorm_indicator_eq_eLpNorm_restrict hsm.compl, eLpNorm_eq_lintegral_rpow_enorm hp₀ hp_top, one_div,
ENNReal.rpow_inv_lt_iff]
simp [ENNReal.toReal_pos, *]
