Markov's inequality #
The classical form of Markov's inequality states that for a nonnegative random variable X and
real number ε > 0, P(X ≥ ε) ≤ E(X) / ε. Multiplying both sides by the measure of the space gives
the measure-theoretic form:
μ { x | ε ≤ f x } ≤ (∫⁻ a, f a ∂μ) / ε
This file proves a few variants of the inequality and other lemmas that depend on it.
theorem
MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f g : α → ENNReal}
(hle : f ≤ᶠ[ae μ] g)
(hg : AEMeasurable g μ)
(ε : ENNReal)
:
A version of Markov's inequality for two functions. It doesn't follow from the standard
Markov's inequality because we only assume measurability of g, not f.
theorem
MeasureTheory.mul_meas_ge_le_lintegral
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → ENNReal}
(hf : Measurable f)
(ε : ENNReal)
:
Markov's inequality also known as Chebyshev's first inequality. For a version assuming
AEMeasurable, see mul_meas_ge_le_lintegral₀.
theorem
MeasureTheory.meas_le_lintegral₀
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
{s : Set α}
(hs : ∀ x ∈ s, 1 ≤ f x)
:
theorem
MeasureTheory.setLIntegral_strict_mono
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f g : α → ENNReal}
{s : Set α}
(hsm : MeasurableSet s)
(hs : μ s ≠ 0)
(hg : Measurable g)
(hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤)
(h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x)
: