meas_ge_le_mul_pow_enorm — Mathlib

English

Another ENNReal-based Markov inequality variant for Lp elements.

Русский

Еще одна вариация неравенства Маркова на ENNReal для элементов Lp.

LaTeX

$$$\text{Markov'}(f)\le \|f\|$$$

Lean4

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

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