Signed row sum under a Boolean coloring
DefinitionrowSumBcombinatoricsdiscrepancy-theory
For a real-valued row (typically with entries in ) and a Boolean coloring , is the signed discrepancy of that row under the coloring — the quantity Spencer's theorem bounds.
Definition code
import Mathlib
import Definitions.Def_RSign
def rowSumB {m : ℕ} (a : Fin m → ℝ) (χ : Fin m → Bool) : ℝ :=
∑ j, a j * RSign χ jSource
J. Spencer, "Six standard deviations suffice", Trans. Amer. Math. Soc. 289 (1985), 679-706.
Human review
Confirmed by the mission captain (proposal self-audit).