Colorings with small discrepancy on every test set

Let p be a probability distribution on a finite palette κ, and color the points of a set ι independently at random according to p. For a finite set T ⊆ ι and a color c, the number of points of T with color c has mean p c * #T, and by Hoeffding's inequality it deviates from its mean by at least a with probability at most 2 * exp (-2 a² / #T) (TauCeti.measureReal_le_abs_card_filter_sub_le). A union bound over a finite family of test sets and over the palette therefore gives a single coloring whose color counts are within a of their means on every test set, as soon as the number of tests times the palette size times 2 * exp (-2 a² / N) is less than one, where N bounds the sizes of the test sets (TauCeti.exists_forall_abs_card_filter_sub_mul_card_lt).

This is the probabilistic method for colorings of low discrepancy. It supplies quasi-random colorings with prescribed color densities, for example colorings of the pairs between two vertex sets in which every color has nearly the same density on every large rectangle.

Main results

• TauCeti.measureReal_le_abs_card_filter_sub_le: Hoeffding's inequality for the number of points of a test set with a given color, under the product of a PMF.
• TauCeti.exists_forall_abs_card_filter_sub_mul_card_lt: a coloring of ι whose color counts on every test set are within a of their means.

Implementation notes

The color count is a function of the coloring with bounded differences: recoloring one point of T changes it by at most one. McDiarmid's inequality TauCeti.Probability.hasSubgaussianMGF_of_bounded_differences therefore makes it sub-Gaussian with variance proxy #T / 4 under the product measure, and Mathlib's Chernoff bound ProbabilityTheory.HasSubgaussianMGF.measure_ge_le gives both tails. The existence statement first restricts to the finite union of the test sets, where the product measure exists, and extends the coloring found there by an arbitrary color.

References

• N. Alon and J. H. Spencer, The Probabilistic Method, 4th ed., Wiley (2016), Theorem 13.1.1 and Appendix A.
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963), 13–30.

theorem TauCeti.measureReal_le_abs_card_filter_sub_le {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] [Fintype ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] (q : PMF κ) (T : Finset ι) (c : κ) {a : ℝ} (ha : 0 ≤ a) : (MeasureTheory.Measure.pi fun (x : ι) => q.toMeasure).real {x : ι → κ | a ≤ |↑{e ∈ T | x e = c}.card - (q c).toReal * ↑T.card|} ≤ 2 * Real.exp (-2 * a ^ 2 / ↑T.card)

Hoeffding's inequality for a color count. Color the points of a finite type ι independently according to a PMF q on κ. The number of points of T with color c deviates from its mean q c * #T by at least a ≥ 0 with probability at most 2 * exp (-2 a² / #T).

theorem TauCeti.exists_forall_abs_card_filter_sub_mul_card_lt {ι : Type u_1} {κ : Type u_2} [DecidableEq κ] [Fintype κ] {p : κ → ℝ} (hp : ∀ (c : κ), 0 ≤ p c) (hp1 : ∑ c : κ, p c = 1) {I : Type u_3} [Fintype I] (T : I → Finset ι) {N : ℕ} (hT : ∀ (i : I), (T i).card ≤ N) {a : ℝ} (ha : 0 < a) (h : 2 * ↑(Fintype.card I) * ↑(Fintype.card κ) * Real.exp (-2 * a ^ 2 / ↑N) < 1) : ∃ (x : ι → κ), ∀ (i : I) (c : κ), |↑{e ∈ T i | x e = c}.card - p c * ↑(T i).card| < a

Colorings with small discrepancy. Let p be a probability distribution on a finite palette κ and T i ⊆ ι, for i in a finite index type I, test sets of size at most N. If 2 * card I * card κ * exp (-2 a² / N) < 1 for some a > 0, then some coloring x : ι → κ has, on every test set T i and for every color c, a number of points of color c within a of p c * #(T i).