English
If f is integrable in MemLp with p = 1 and is measurable, then there exists M such that the integral of the nonnegative indicator of {x | M ≤ ||f(x)||_+} against μ is bounded by a finite real bound depending on ε.
Русский
Пусть f измерима и принадлежит MemLp f 1 μ; тогда существует M, такое что интеграл по μ от индикатора {x | M ≤ ||f(x)||_+} ограничен конечной величиной зависимой от ε.
LaTeX
$$$ \\exists M \\in \\mathbb{R}, \\quad \\int^\\infty \\|\\{x | M \\le \\|f(x)\\|_+\\}.indicator f(x)\\|_+ \\, dμ ≤ ENNReal.ofReal(ε) $$$
Lean4
/-- This lemma is superseded by `MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le`
which does not require measurability. -/
theorem integral_indicator_norm_ge_nonneg_le_of_meas (hf : MemLp f 1 μ) (hmeas : StronglyMeasurable f) {ε : ℝ}
(hε : 0 < ε) : ∃ M : ℝ, 0 ≤ M ∧ (∫⁻ x, ‖{x | M ≤ ‖f x‖₊}.indicator f x‖ₑ ∂μ) ≤ ENNReal.ofReal ε :=
let ⟨M, hM⟩ := hf.integral_indicator_norm_ge_le hmeas hε
⟨max M 0, le_max_right _ _, by simpa⟩
