theorem markov_inequality {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_nn : 0 ≤ᵐ[μ] X) (hX_int : MeasureTheory.Integrable X μ) {a : ℝ} (ha : 0 < a) : μ.real {ω : Ω | a ≤ X ω} ≤ (∫ (ω : Ω), X ω ∂μ) / a

Markov's inequality. Let X be a non-negative integrable random variable on the probability space (Ω, μ) and let a > 0. Then

μ{ω | a ≤ X ω} ≤ (∫ X dμ) / a.