mul_meas_ge_le_pow_eLpNorm — Mathlib

English

Chebyshev-type inequality: μ{x | ε ≤ ‖f x‖^p.toReal} ≤ ε^{-p.toReal} · (eLpNorm f p μ)^{p.toReal}.

Русский

Неравенство Чебышёва: μ{x: ε ≤ ‖f(x)‖^p.toReal} ≤ ε^{-p.toReal} (eLpNorm f)^p.

LaTeX

$$$$μ\\{x \\,|\\, ε \\le \\|f(x)\\|^{p.toReal} \\} ≤ ε^{-p.toReal} \\; (eLpNorm f)^{p.toReal}.$$$$

Lean4

theorem mul_meas_ge_le_pow_eLpNorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε'} (hf : AEStronglyMeasurable f μ)
    (ε : ℝ≥0∞) : ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal :=
  by
  have : 1 / p.toReal * p.toReal = 1 := by
    refine one_div_mul_cancel ?_
    rw [Ne, ENNReal.toReal_eq_zero_iff]
    exact not_or_intro hp_ne_zero hp_ne_top
  rw [← ENNReal.rpow_one (ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}), ← this, ENNReal.rpow_mul]
  gcongr
  exact pow_mul_meas_ge_le_eLpNorm μ hp_ne_zero hp_ne_top hf ε

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