English
If MemLp f p μ and f is strongly measurable, then for every ε>0 there exists δ>0 so that for all measurable s with μ(s) ≤ δ the tail indcator Lp-norm is ≤ ε; this variant does not require f itself to be measurably trivial.
Русский
Если f ∈ MemLp(f,p,μ) и f сильно измерима, то для любого ε>0 существует δ>0 так что для всех измеримых s с μ(s) ≤ δ хвостовая индикаторная Lp-норма ≤ ε; это не требует тривиальной измеримости самой f.
LaTeX
$$$\exists δ>0,\ ∀ s,\ MeasurableSet s,\ μ s ≤ ENNReal.ofReal δ \Rightarrow eLpNorm(s.indicator f) p μ ≤ ENNReal.ofReal ε$$$
Lean4
/-- This lemma is superseded by `MeasureTheory.MemLp.eLpNorm_indicator_le` which does not require
measurability on `f`. -/
theorem eLpNorm_indicator_le_of_meas (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ) (hmeas : StronglyMeasurable f)
{ε : ℝ} (hε : 0 < ε) :
∃ (δ : ℝ) (_ : 0 < δ),
∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε :=
by
obtain ⟨δ, hδpos, hδ⟩ := hf.eLpNorm_indicator_le' hp_one hp_top hmeas (half_pos hε)
refine ⟨δ, hδpos, fun s hs hμs => le_trans (hδ s hs hμs) ?_⟩
rw [ENNReal.ofReal_div_of_pos zero_lt_two, (by simp : ENNReal.ofReal 2 = 2), ENNReal.mul_div_cancel] <;> norm_num
