English
Azuma-Hoeffding bound for sub-Gaussian martingale differences: the sum of Y_i with conditional subgaussian MGFs has a bound with sum of cY i.
Русский
bound Азумы-Хоэффдинга для разностей мартингейра – сумма Y_i с условной субгауссовой MGФ имеет параметр сумма_Y.
LaTeX
$$$\mathrm{HasSubgaussianMGF\_sum\_of\_HasCondSubgaussianMGF}(...) \,: \; \mathrm{HasSubgaussianMGF}(\sum_i Y_i, \sum_i cY_i, μ)$$$
Lean4
/-- **Azuma-Hoeffding inequality** for sub-Gaussian random variables. -/
theorem measure_sum_ge_le_of_HasCondSubgaussianMGF [IsZeroOrProbabilityMeasure μ] (h_adapted : Adapted ℱ Y)
(h0 : HasSubgaussianMGF (Y 0) (cY 0) μ) (n : ℕ)
(h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (ℱ i) (ℱ.le i) (Y (i + 1)) (cY (i + 1)) μ) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, cY i)) :=
(HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF h_adapted h0 n h_subG).measure_ge_le hε
