English
A variant of the previous bound: for any ε>0 there exists M such that the Lp-norm of the indicator tail is bounded by ε, using ENNReal norms and some normalizations.
Русский
Вариант предыдущего предела: для заданного ε>0 существует M так, что Lp-норма индикатора хвоста ограничена сверху ε, с использованием норм ENNReal.
LaTeX
$$$\exists M,\ eLpNormIndicatorGeLe\text{(f, p, μ, M)} ≤ ε$$$
Lean4
theorem eLpNorm_indicator_le_of_bound {f : α → β} (hp_top : p ≠ ∞) {ε : ℝ} (hε : 0 < ε) {M : ℝ} (hf : ∀ x, ‖f x‖ < M) :
∃ (δ : ℝ) (_ : 0 < δ),
∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε :=
by
by_cases hM : M ≤ 0
· refine ⟨1, zero_lt_one, fun s _ _ => ?_⟩
rw [(_ : f = 0)]
· simp
· ext x
rw [Pi.zero_apply, ← norm_le_zero_iff]
exact (lt_of_lt_of_le (hf x) hM).le
rw [not_le] at hM
refine ⟨(ε / M) ^ p.toReal, Real.rpow_pos_of_pos (div_pos hε hM) _, fun s hs hμ => ?_⟩
by_cases hp : p = 0
· simp [hp]
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
have haebdd : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ M := by
filter_upwards
exact fun x => (hf x).le
refine le_trans (eLpNorm_le_of_ae_bound haebdd) ?_
rw [Measure.restrict_apply MeasurableSet.univ, Set.univ_inter, ←
ENNReal.le_div_iff_mul_le (Or.inl _) (Or.inl ENNReal.ofReal_ne_top)]
· rw [ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp_top)]
refine le_trans hμ ?_
rw [← ENNReal.ofReal_rpow_of_pos (div_pos hε hM), ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp hp_top),
ENNReal.ofReal_div_of_pos hM]
· simpa only [ENNReal.ofReal_eq_zero, not_le, Ne]
