mul_meas_ge_le_pow_enorm' — Mathlib

English

A variant of Markov’s inequality using ENNReal-valued exponent and NNNorm in Lp: ε^p ⋅ μ{ x : ε ≤ ε^p⋅‖f(x)‖^p } ≤ ε^p ⋅ ‖f‖^p.

Русский

Вариант неравенства Маркова с использованием ENNReal-показателя и NNNorm в Lp: ...

LaTeX

$$$\varepsilon^p \cdot \mu\{x\mid \varepsilon \le \varepsilon^p \cdot \|f(x)\|^p\} \le \varepsilon^p \cdot \|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∞) :
    ε ^ p.toReal * μ {x | ε ≤ ‖f x‖₊} ≤ 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) ε

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