Proof of Korten's improved light-patterns lemma

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

Transfer the downward-closed event that the harmonic transform is large, then bound light patterns by the reciprocal-density Markov inequality. The final step converts normalized marginal densities into probability masses and counts, preserving the paper's real deficit parameter and constants.

theorem Complexity.BooleanAnalysis.harmonicTransform_sparse_good_probability_fin_internal {n : ℕ} {f : (Fin n → Bool) → ℝ} (hf : ∀ (x : Fin n → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : Fin n → Bool) => f x) = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : Fin n → Bool), f x ≤ 2 ^ k) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : Fin n → Bool) => if 1 / (4 * 2 ^ k) ≤ harmonicTransform f s then 1 else 0

theorem Complexity.BooleanAnalysis.harmonicTransform_sparse_good_probability_internal {ι : 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

theorem Complexity.BooleanAnalysis.improved_light_patterns_density_internal {ι : 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

theorem Complexity.BooleanAnalysis.coordinateMarginal_normalize_internal {ι : 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

theorem Complexity.BooleanAnalysis.improved_light_patterns_internal {ι : 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

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