pow_mul_meas_ge_le_enorm — Mathlib

English

A version of Markov’s inequality for elements of Lp: for ε>0, (ε μ{x: ε ≤ ||f(x)||^p})^{1/p} ≤ ||f||_p.

Русский

Версия неравенства Маркова для элементов Lp: для любых ε>0 имеет место (ε μ{x: ε ≤ ||f(x)||^p})^{1/p} ≤ ||f||_p.

LaTeX

$$$\left(\varepsilon \cdot \mu\{x\mid \varepsilon \le \|f(x)\|^p\}\right)^{1/p} \le \|f\|_p$$$

Lean4

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

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