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.snorm seminorm.

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.snorm f p μ

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.snorm f p μ ^ p.toReal

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.snorm f p μ ^ p.toReal

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

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.snorm f p μ ^ p.toReal