Eq. (1): $\Pr\{\sum_j\eta_jp_j > \Omega\sqrt{\sum_jp_j^2}\}\le\exp\{-\Omega^2/2\}$ for independent symmetric $[-1,1]$ variables

Proved

RobustLP.Counterpart.symmetric_sum_tail_bound

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

concentration-inequalitiesp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let $(S,\mathcal F,\mathbb P)$ be a probability space and $\eta_j$ , $j$ in a finite index set, be independent real random variables, each symmetrically distributed ( $\eta_j$ and $-\eta_j$ have the same law) and taking values in $[-1,1]$ . Let $p_j$ be given reals. Then for every $\Omega>0$ ,

\mathbb P\Big\{\sum_j \eta_j p_j > \Omega\sqrt{\sum_j p_j^2}\Big\} \le \exp\{-\Omega^2/2\}.

This Hoeffding-type tail bound is the "well-known fact" used to conclude Proposition 1: applied to $\eta_j=\xi_{ij}$ and $p_j=a_{ij}z_{ij}$ , it bounds the violation probability of each constraint of a solution of (RC[ε, δ, Ω]).

Formalization Note The event is strict, as printed. When all $p_j=0$ the event is empty. The weights are called pc in Lean. Symmetry is the equality of image measures P.map (η j) = P.map (fun ω => -η j ω), independence is iIndepFun η P, and values in $[-1,1]$ are required at every outcome. The probability is P.real.

Preamble

import Mathlib

open MeasureTheory ProbabilityTheory

Formal statement

namespace RobustLP.Counterpart

/-- **Fact (1)** (Ben-Tal–Nemirovski 2000, §3.1, p. 419, Eq. (1)). Let `p_j` be given reals and
`η_j` independent random variables, each symmetrically distributed (the law of `η_j` equals the
law of `-η_j`) and taking values in `[-1, 1]`. Then for every `Ω > 0`,
`P(∑_j η_j p_j > Ω √(∑_j p_j²)) ≤ exp(-Ω²/2)`. -/
theorem symmetric_sum_tail_bound {ι : Type*} [Fintype ι]
    {S : Type*} [MeasurableSpace S] (P : Measure S) [IsProbabilityMeasure P]
    (η : ι → S → ℝ) (hmeas : ∀ j, Measurable (η j)) (hindep : iIndepFun η P)
    (hsymm : ∀ j, P.map (η j) = P.map (fun ω => -η j ω))
    (hbdd : ∀ j ω, η j ω ∈ Set.Icc (-1 : ℝ) 1)
    (pc : ι → ℝ) (Ω : ℝ) (hΩ : 0 < Ω) :
    P.real {ω | Ω * Real.sqrt (∑ j, pc j ^ 2) < ∑ j, η j ω * pc j} ≤
      Real.exp (-(Ω ^ 2 / 2)) := by sorry

end RobustLP.Counterpart

Source

Ben-Tal and Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424, p. 419, §3.1, Eq. (1)

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (1): Pr⁡{∑jηjpj>Ω∑jpj2}≤exp⁡{−Ω2/2}\Pr\{\sum_j\eta_jp_j > \Omega\sqrt{\sum_jp_j^2}\}\le\exp\{-\Omega^2/2\}Pr{∑j​ηj​pj​>Ω∑j​pj2​​}≤exp{−Ω2/2} for independent symmetric [−1,1][-1,1][−1,1] variables

Eq. (1): $\Pr\{\sum_j\eta_jp_j > \Omega\sqrt{\sum_jp_j^2}\}\le\exp\{-\Omega^2/2\}$ for independent symmetric $[-1,1]$ variables