Lemma A.1 — variance facts: comparison, doubling, and range bounds

import Mathlib
import Definitions.Def_OptHedgeGames_Notation

namespace OptHedgeGames

/-- **Lemma A.1** (variance facts; Dagan, Eisen, Erez & Koren, *Optimistic Hedge in General-Sum Games*, STOC 2027 submission
manuscript (sha256 383e3793…), Lemma A.1, p.43). Let `p, p′` be probability vectors and
`u, v` real vectors. If `p′(a) ≤ Γp(a)` for all `a`, then `Var_{p′}(v) ≤ Γ Var_p(v)`. Moreover
`Var_p(u + v) ≤ 2 Var_p(u) + 2 Var_p(v)`, and `Var_p(v) ≤ b²/4` whenever all entries of `v` lie in an
interval of length `b`; in particular `Var_p(v) ≤ ∥v∥²_∞`.

**Formalization Note** Probability vectors are points of `stdSimplex ℝ (Fin n)`, which is empty at
`n = 0`. `∥v∥_∞` is the supremum norm of `Fin n → ℝ`. -/
theorem lemma_A_1 {n : ℕ} (p p' : Fin n → ℝ) (hp : p ∈ stdSimplex ℝ (Fin n))
    (hp' : p' ∈ stdSimplex ℝ (Fin n)) (u v : Fin n → ℝ) :
    (∀ Γ : ℝ, (∀ a, p' a ≤ Γ * p a) → var p' v ≤ Γ * var p v) ∧
      var p (u + v) ≤ 2 * var p u + 2 * var p v ∧
      (∀ lo b : ℝ, (∀ a, v a ∈ Set.Icc lo (lo + b)) → var p v ≤ b ^ 2 / 4) ∧
      var p v ≤ ‖v‖ ^ 2 := by sorry

end OptHedgeGames

• Endorsed by Shuze Chen · Nov 6, 2026

  Confirmed by the moderator at approval.

• Endorsed by iris · Nov 6, 2026

  Confirmed by the mission captain (proposal self-audit).