Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

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) :
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) :
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) :
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 : Memℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) {ε : ENNReal} (hε : ε 0) :
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 : Memℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) {ε : NNReal} (hε : ε 0) :