Banaszczyk’s vector balancing theorem for Gaussian-large convex bodies

Open

Komlos.banaszczyk_convex_body

by Wenqian · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

banaszczykconvex-geometrygaussian-measurevector-balancing

Let $n,m\ge0$ and let $v_1,\ldots,v_n\in\mathbb R^m$ have Euclidean norms at most $1/5$ . If $K\subseteq\mathbb R^m$ is compact and convex and has standard Gaussian measure at least $1/2$ , then there are signs $\varepsilon_i\in\{-1,1\}$ such that

\sum_{i=1}^n\varepsilon_i v_i\in K.

No central symmetry hypothesis is imposed on $K$ . The same norm threshold applies in every dimension and for every family size. The statement includes empty families and dimension zero. This is the general convex-body balancing input from which the separate cube-measure estimate yields the dimension-dependent coordinate discrepancy bound.

Preamble

import Definitions.Def_Komlos_model
import Mathlib.Probability.Distributions.Gaussian.Multivariate

open MeasureTheory ProbabilityTheory Set
open scoped BigOperators

Formal statement

namespace Komlos

theorem banaszczyk_convex_body
    (n m : ℕ) (v : Fin n → EuclideanSpace ℝ (Fin m))
    (hv : ∀ i, ‖v i‖ ≤ (1/5 : ℝ))
    (K : Set (EuclideanSpace ℝ (Fin m))) (hconv : Convex ℝ K) (hcomp : IsCompact K)
    (hGauss : (1/2 : ℝ) ≤ (stdGaussian (EuclideanSpace ℝ (Fin m))).real K) :
    ∃ ε : Fin n → ℝ, IsSignVector ε ∧ ∑ i, ε i • v i ∈ K := by sorry

end Komlos

Source

Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998), Theorem 1. Exact norm-1/5 formulation: Dadush–Garg–Lovett–Nikolov, Towards a Constructive Version of Banaszczyk's Vector Balancing Theorem, Theory of Computing 15(15), 2019, Theorem 1.1, p. 2, https://theoryofcomputing.org/articles/v015a015/v015a015.pdf . The posted form restricts to compact convex sets; positive Gaussian measure supplies full dimension when m>0.

View graph