mul_meas_ge_le_pow_enorm — Mathlib

English

Variant of Markov inequality for ENNReal-powers in Lp: ε^p ⋅ μ{ x : ε ≤ ||f(x)||^p } ≤ ||f||^p.

Русский

Вариант неравенства Маркова для степеней ENNReal в Lp: ε^p ⋅ μ{ x : ε ≤ ||f(x)||^p } ≤ ||f||^p.

LaTeX

$$$\varepsilon^p \cdot \mu\{x\mid \varepsilon \le \|f(x)\|^p\} \le \|f\|^p$$$

Lean4

/-- A version of **Markov's inequality** with elements of Lp. -/
theorem mul_meas_ge_le_pow_enorm (f : Lp E p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) (ε : ℝ≥0∞) :
    ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal :=
  (ENNReal.ofReal_toReal (eLpNorm_ne_top f)).symm ▸
    mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top (Lp.aestronglyMeasurable f) ε

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