English
An auxiliary bound: given a finite M, for p ≠ ∞, there exists δ>0 such that for all measurable s with μ(s) ≤ δ, the p-th eLp norm of s.indicator f is bounded by ε, provided ∥f(x)∥ is globally dominated by M.
Русский
Вспомогательное неравенство: при заданном конечном M и p ≠ ∞ существует δ>0 такое, что для каждого измеримого s с μ(s) ≤ δ нормa eLp равна не более ε, если ∥f(x)∥ ≤ M повсюду.
LaTeX
$$$\exists δ>0,\ ∀ s,\ MeasurableSet s,\ μ s ≤ ENNReal.ofReal δ \Rightarrow eLpNorm(s.indicator f) p μ ≤ ENNReal.ofReal ε$$$
Lean4
/-- Auxiliary lemma for `MeasureTheory.MemLp.eLpNorm_indicator_le`. -/
theorem eLpNorm_indicator_le' (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 μ ≤ 2 * ENNReal.ofReal ε :=
by
obtain ⟨M, hMpos, hM⟩ := hf.eLpNorm_indicator_norm_ge_pos_le hmeas hε
obtain ⟨δ, hδpos, hδ⟩ :=
eLpNorm_indicator_le_of_bound (f := {x | ‖f x‖ < M}.indicator f) hp_top hε
(by
intro x
rw [norm_indicator_eq_indicator_norm, Set.indicator_apply]
· split_ifs with h
exacts [h, hMpos])
refine ⟨δ, hδpos, fun s hs hμs => ?_⟩
rw [(_ : f = {x : α | M ≤ ‖f x‖₊}.indicator f + {x : α | ‖f x‖ < M}.indicator f)]
· rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
refine le_trans (eLpNorm_add_le ?_ ?_ hp_one) ?_
·
exact
StronglyMeasurable.aestronglyMeasurable
(hmeas.indicator (measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe))
·
exact
StronglyMeasurable.aestronglyMeasurable
(hmeas.indicator (measurableSet_lt hmeas.nnnorm.measurable.subtype_coe measurable_const))
· rw [two_mul]
refine add_le_add (le_trans (eLpNorm_mono_measure _ Measure.restrict_le_self) hM) ?_
rw [← eLpNorm_indicator_eq_eLpNorm_restrict hs]
exact hδ s hs hμs
· ext x
by_cases hx : M ≤ ‖f x‖
· rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_notMem, add_zero] <;> simpa
· rw [Pi.add_apply, Set.indicator_of_notMem, Set.indicator_of_mem, zero_add] <;> simpa using hx
