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

Theorem 3.3.1 (Markov's inequality). For a nonnegative integrable random variable $X$ and any $a > 0$, $\mathbb{P}(X \geq a) \leq \mathbb{E}[X] / a$.