English
Let X be a real-valued random variable with a subgaussian mgf relative to a kernel κ and base ν. Then for almost every ω' distributed by ν, and for every nonnegative t, the right tail probability of X under the conditional distribution κ(ω') is universally bounded by exp(-t·ε + (c t^2)/2) for every ε ∈ R.
Русский
Пусть X — произвольная случайная величина со свающим MGФ с параметром Subgaussian относительно ядра κ и меры-основания ν. Тогда для почти всех ω', распределённых по ν, при любом t ≥ 0 выполняется неравенство на правый хвост: для множества ω, принадлежащего условному распределению κ(ω'), имеет верхнюю оценку exp(-t·ε + c t^2 / 2) для любого ε ∈ R.
LaTeX
$$$\forall ε ∈ \mathbb{R},\ ∀^{⋄} ω' \partial ν,\ ∀ t ≥ 0:\ (κ(ω'))\{ω : ε \le X(ω)\} \le \exp(-t ε + \tfrac{c t^2}{2})$$$
Lean4
theorem measure_ge_le_exp_add (h : HasSubgaussianMGF X c κ ν) (ε : ℝ) :
∀ᵐ ω' ∂ν, ∀ t, 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ exp (-t * ε + c * t ^ 2 / 2) :=
by
filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul, h.isFiniteMeasure] with ω' h1 h2 _ t ht
calc
(κ ω').real {ω | ε ≤ X ω}
_ ≤ exp (-t * ε) * mgf X (κ ω') t := (measure_ge_le_exp_mul_mgf ε ht (h2 t))
_ ≤ exp (-t * ε + c * t ^ 2 / 2) := by
rw [exp_add]
gcongr
exact h1 t
