mul_meas_ge_le_pow_eLpNorm' — Mathlib

English

Variant with power-passed lifting: ε^p.toReal · μ{x | ε ≤ ‖f x‖^p.toReal} ≤ (eLpNorm f p μ)^p.toReal.

Русский

Вариант с выводом по степени: ε^{p.toReal} · μ{x | ε ≤ ‖f x‖^{p.toReal}} ≤ (eLpNorm f)^{p.toReal}.

LaTeX

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

Lean4

/-- A version of Chebyshev-Markov's inequality using Lp-norms. -/
theorem mul_meas_ge_le_pow_eLpNorm' (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε'}
    (hf : AEStronglyMeasurable f μ) (ε : ℝ≥0∞) : ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ eLpNorm f p μ ^ p.toReal :=
  by
  convert mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal) using 4
  ext x
  rw [ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]

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