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} (μ : MeasureTheory.Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f μ) (ε : ENNReal) : (ε * μ {x : α | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ

@[deprecated MeasureTheory.pow_mul_meas_ge_le_eLpNorm]

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

Alias of MeasureTheory.pow_mul_meas_ge_le_eLpNorm.

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

@[deprecated MeasureTheory.mul_meas_ge_le_pow_eLpNorm]

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

Alias of MeasureTheory.mul_meas_ge_le_pow_eLpNorm.

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

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

@[deprecated MeasureTheory.mul_meas_ge_le_pow_eLpNorm']

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

Alias of MeasureTheory.mul_meas_ge_le_pow_eLpNorm'.

---

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} (μ : MeasureTheory.Measure α) {f : α → E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f μ) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal

@[deprecated MeasureTheory.meas_ge_le_mul_pow_eLpNorm]

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

Alias of MeasureTheory.meas_ge_le_mul_pow_eLpNorm.

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

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