Korten's improved light-patterns lemma

Lemma 10 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

improved_light_patterns uses an arbitrary nonnegative real probability mass function summing to one. The pointwise bound mass x ≤ 2 ^ (k - Fintype.card ι) expresses min-entropy deficit at most k. With probability at least 63/64 over independent coordinate sampling of rate r ≤ 1/(512*k), at most 2^(|R|-k) patterns have marginal probability at most 2^(-|R|-2*k-2).

improved_light_patterns_density gives the equivalent fraction statement for normalized densities. coordinateMarginal_normalize verifies the passage from probability masses to normalized marginal densities. All results include arbitrary finite coordinate types, dimension zero, zero masses, and sampling rate zero. Complexitylib.BooleanAnalysis.MirrorSets applies this lemma in the improved mirror-set argument.

theorem Complexity.BooleanAnalysis.sum_coordinateMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (s : ι → Bool) : ∑ z : { i : ι // s i = true } → Bool, coordinateMass mass s z = ∑ x : ι → Bool, mass x

Marginalization preserves total probability mass.

theorem Complexity.BooleanAnalysis.coordinateMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mass : (ι → Bool) → ℝ} (hm : ∀ (x : ι → Bool), 0 ≤ mass x) (s : ι → Bool) (z : { i : ι // s i = true } → Bool) : 0 ≤ coordinateMass mass s z

Marginal masses of a nonnegative mass function are nonnegative.

theorem Complexity.BooleanAnalysis.coordinateMarginal_normalize {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (s : ι → Bool) (z : { i : ι // s i = true } → Bool) : coordinateMarginal (fun (x : ι → Bool) => 2 ^ Fintype.card ι * mass x) s z = 2 ^ Fintype.card { i : ι // s i = true } * coordinateMass mass s z

Normalizing the input mass by 2^n normalizes each marginal by 2^|R|.

theorem Complexity.BooleanAnalysis.harmonicTransform_sparse_good_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : ι → Bool) => f x) = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), f x ≤ 2 ^ k) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if 1 / (4 * 2 ^ k) ≤ harmonicTransform f s then 1 else 0

Sparse-sampling estimate for the harmonic transform in the proof of Lemma 10.

theorem Complexity.BooleanAnalysis.improved_light_patterns_density {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : ι → Bool) => f x) = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), f x ≤ 2 ^ k) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if (Finset.univ.expect fun (z : { i : ι // s i = true } → Bool) => if coordinateMarginal f s z ≤ 2 ^ (-2 * k - 2) then 1 else 0) ≤ 2 ^ (-k) then 1 else 0

Lemma 10 for normalized densities: with probability at least 63/64, the fraction of patterns with marginal density at most 2^(-2*k-2) is at most 2^-k.

theorem Complexity.BooleanAnalysis.improved_light_patterns {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mass : (ι → Bool) → ℝ} (hm : ∀ (x : ι → Bool), 0 ≤ mass x) (hmean : ∑ x : ι → Bool, mass x = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), mass x ≤ 2 ^ (k - ↑(Fintype.card ι))) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if ↑{z : { i : ι // s i = true } → Bool | coordinateMass mass s z ≤ 2 ^ (-↑(Fintype.card { i : ι // s i = true }) - 2 * k - 2)}.card ≤ 2 ^ (↑(Fintype.card { i : ι // s i = true }) - k) then 1 else 0

Korten's improved light-patterns lemma (Lemma 10), with its exact constants and pattern count. Nonnegative masses summing to one represent a distribution; the pointwise bound is min-entropy deficit at most the real parameter k.