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} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hle : f ≤ᵐ[μ] g) (hg : AEMeasurable g μ) (ε : ENNReal) : ∫⁻ (a : α), f a ∂μ + ε * μ {x : α | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ

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} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (ε : ENNReal) : ε * μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Markov's inequality also known as Chebyshev's first inequality.

theorem MeasureTheory.mul_meas_ge_le_lintegral {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (ε : ENNReal) : ε * μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

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} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {s : Set α} (hs : ∀ x ∈ s, 1 ≤ f x) : μ s ≤ ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_le_meas {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hf : ∀ (a : α), f a ≤ 1) (h'f : ∀ a ∈ sᶜ, f a = 0) : ∫⁻ (a : α), f a ∂μ ≤ μ s

theorem MeasureTheory.setLIntegral_le_meas {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) {f : α → ENNReal} (hf : ∀ a ∈ s, a ∈ t → f a ≤ 1) (hf' : ∀ a ∈ s, a ∉ t → f a = 0) : ∫⁻ (a : α) in s, f a ∂μ ≤ μ t

theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hμf : μ {x : α | f x = ⊤} ≠ 0) : ∫⁻ (x : α), f x ∂μ = ⊤

theorem MeasureTheory.setLIntegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (hμf : μ {x : α | x ∈ s ∧ f x = ⊤} ≠ 0) : ∫⁻ (x : α) in s, f x ∂μ = ⊤

theorem MeasureTheory.measure_eq_top_of_lintegral_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hμf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : μ {x : α | f x = ⊤} = 0

theorem MeasureTheory.measure_eq_top_of_setLIntegral_ne_top {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (hμf : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) : μ {x : α | x ∈ s ∧ f x = ⊤} = 0

theorem MeasureTheory.meas_ge_le_lintegral_div {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {ε : ENNReal} (hε : ε ≠ 0) (hε' : ε ≠ ⊤) : μ {x : α | ε ≤ f x} ≤ (∫⁻ (a : α), f a ∂μ) / ε

Markov's inequality, also known as Chebyshev's first inequality.

theorem MeasureTheory.ae_eq_of_ae_le_of_lintegral_le {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hg : AEMeasurable g μ) (hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ) : f =ᵐ[μ] g

theorem MeasureTheory.lintegral_eq_iff_ae_eq_of_ae_le {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hg : AEMeasurable g μ) (h : f ≤ᵐ[μ] g) : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ ↔ f =ᵐ[μ] g

theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ (x : α) ∂μ, f x ≠ g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) {s : Set α} (hμs : μ s ≠ 0) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.lintegral_strict_mono {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hμ : μ ≠ 0) (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h : ∀ᵐ (x : α) ∂μ, f x < g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.setLIntegral_strict_mono {α : Type u_1} {mα : 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) : ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in s, g x ∂μ

theorem MeasureTheory.ae_lt_top' {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ∀ᵐ (x : α) ∂μ, f x < ⊤

theorem MeasureTheory.ae_lt_top {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ∀ᵐ (x : α) ∂μ, f x < ⊤