measure_sum_ge_le_of_iIndepFun — Mathlib

English

For an iIndepFun X with μ, and a finite index set s, if each X_i has sub-Gaussian MGФ with c_i, then the sum over s has sub-Gaussian MGФ with parameter ∑ c_i.

Русский

Для iIndepFun X и конечного множества s, если у каждого X_i субгауссов MGF c_i, то сумма по s имеет субгауссову MGФ с параметром ∑ c_i.

LaTeX

$$$\mathrm{iIndepFun}(X,\mu) \land \forall i\in s, \mathrm{HasSubgaussianMGF}(X_i,c_i,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(\lambda i\in s. X_i, \sum_{i\in s} c_i,\mu)$$$

Lean4

/-- **Hoeffding inequality** for sub-Gaussian random variables. -/
theorem measure_sum_ge_le_of_iIndepFun {ι : Type*} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {c : ι → ℝ≥0}
    {s : Finset ι} (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) {ε : ℝ} (hε : 0 ≤ ε) :
    μ.real {ω | ε ≤ ∑ i ∈ s, X i ω} ≤ exp (-ε ^ 2 / (2 * ∑ i ∈ s, c i)) :=
  (sum_of_iIndepFun h_indep h_subG).measure_ge_le hε

Похожие утверждения