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} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} (μ : Measure α) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε'} (ε : ENNReal) : (ε * μ {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ

theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} (μ : Measure α) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε'} (ε : ENNReal) : ε * μ {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm' {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} (μ : Measure α) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {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_enorm {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} (μ : Measure α) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε'} {ε : ENNReal} (hε : ε ≠ 0) (hmeas_top : ε = ⊤ → μ {x : α | ‖f x‖ₑ = ⊤} = 0) : μ {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.MemLp.meas_ge_lt_top'_enorm {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} {μ : Measure α} {f : α → ε'} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) (hε' : ε = ⊤ → μ {x : α | ‖f x‖ₑ = ⊤} = 0) : μ {x : α | ε ≤ ‖f x‖ₑ} < ⊤

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

theorem MeasureTheory.MemLp.meas_ge_lt_top_enorm {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [TopologicalSpace ε'] [ContinuousENorm ε'] {p : ENNReal} {μ : Measure α} {f : α → ε'} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) : μ {x : α | ↑ε ≤ ‖f x‖ₑ} < ⊤

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