Chebyshev-Markov inequality in terms of Lp seminorms

In this file we formulate several versions of the Chebyshev-Markov inequality in terms of the MeasureTheory.eLpNorm seminorm.

theorem MeasureTheory.pow_mul_meas_ge_le_eLpNorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} (μ : Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : AEStronglyMeasurable f μ) (ε : ENNReal) : (ε * μ {x : α | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ

theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} (μ : Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : AEStronglyMeasurable f μ) (ε : ENNReal) : ε * μ {x : α | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} (μ : Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : AEStronglyMeasurable f μ) (ε : ENNReal) : ε ^ p.toReal * μ {x : α | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal

A version of Chebyshev-Markov's inequality using Lp-norms.

theorem MeasureTheory.meas_ge_le_mul_pow_eLpNorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} (μ : Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : AEStronglyMeasurable f μ) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.MemLp.meas_ge_lt_top' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖f x‖₊} < ⊤

@[deprecated MeasureTheory.MemLp.meas_ge_lt_top' (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.meas_ge_lt_top' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖f x‖₊} < ⊤

Alias of MeasureTheory.MemLp.meas_ge_lt_top'.

theorem MeasureTheory.MemLp.meas_ge_lt_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ‖f x‖₊} < ⊤

@[deprecated MeasureTheory.MemLp.meas_ge_lt_top (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.meas_ge_lt_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} {μ : Measure α} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ‖f x‖₊} < ⊤

Alias of MeasureTheory.MemLp.meas_ge_lt_top.