pow_mul_meas_ge_le_eLpNorm — Mathlib

English

For p ≠ 0, ∞ and AEStronglyMeasurable f, the Chebyshev-Markov type inequality holds: (ε * μ{x | ε ≤ ‖f x‖^p.toReal})^{1/p.toReal} ≤ eLpNorm(f).

Русский

Для p ≠ 0, ∞ и AEStronglyMeasurable f выполняется неравенство Чебышева-Маркова: (ε · μ{x: ε ≤ ‖f x‖^p.toReal})^{1/p.toReal} ≤ eLpNorm(f).

LaTeX

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

Lean4

theorem pow_mul_meas_ge_le_eLpNorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε'} (hf : AEStronglyMeasurable f μ)
    (ε : ℝ≥0∞) : (ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ :=
  by
  rw [eLpNorm_eq_lintegral_rpow_enorm hp_ne_zero hp_ne_top]
  gcongr
  exact mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const _) ε

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