meas_ge_le_mul_pow_eLpNorm — Mathlib

English

For general ε, μ{x | ε ≤ ‖f x‖^p.toReal} ≤ ε^{-p.toReal} · (eLpNorm f p μ)^{p.toReal}.

Русский

Для общего ε: μ{x: ε ≤ ‖f(x)‖^p.toReal} ≤ ε^{-p.toReal} · (eLpNorm f)^p.toReal.

LaTeX

$$$$μ\\{x \\,|\\, ε \\le \\|f(x)\\|^{p.toReal} \\} \\\\le ε^{-p.toReal} \\, (eLpNorm f)^{p.toReal}.$$$$

Lean4

@[deprecated meas_ge_le_mul_pow_eLpNorm_enorm (since := "2025-05-01")]
theorem meas_ge_le_mul_pow_eLpNorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → E} (hf : AEStronglyMeasurable f μ)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) : μ {x | ε ≤ ‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal :=
  meas_ge_le_mul_pow_eLpNorm_enorm μ hp_ne_zero hp_ne_top hf hε (by simp)

Похожие утверждения