Theorems · Theorem · probability

ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω - ∫ (x : Ω), X x ∂μ) cX μ →
    ProbabilityTheory.HasSubgaussianMGF (fun ω => Y ω - ∫ (x : Ω), Y x ∂μ) cY μ →
      ProbabilityTheory.IndepFun X Y μ →
        ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ →
          μ.real {ω | X ω ≤ Y ω} ≤ Real.exp (-(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2 / (2 * (↑cX + ↑cY)))

For X, Y two independent sub-Gaussian random variables such that μ[X] ≥ μ[Y], the probability that X ≤ Y is bounded by an exponential decay term.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

0 results in Mathlib

Foundations

Depth 274 from the axioms · uses propext, Classical.choice, Quot.sound