Product sampling and downward-closed transference

Union of independent coordinate sets and iteration prove the transfer principle used in Section 4 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/. Korten credits the principle to Yufei Zhao, Probabilistic Methods in Combinatorics, Lemma 4.3.7. This proof includes the zero sampling rate.

theorem Complexity.BooleanAnalysis.sum_cons_internal {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) : ∑ x : Fin (n + 1) → Bool, f x = ∑ x : Fin n → Bool, f (Fin.cons false x) + ∑ x : Fin n → Bool, f (Fin.cons true x)

theorem Complexity.BooleanAnalysis.bernoulliWeight_cons_internal {n : ℕ} (p : ℝ) (b : Bool) (selected : Fin n → Bool) : bernoulliWeight p (Fin.cons b selected) = (if b = true then p else 1 - p) * bernoulliWeight p selected

theorem Complexity.BooleanAnalysis.bernoulliAverage_cons_internal {n : ℕ} (p : ℝ) (f : (Fin (n + 1) → Bool) → ℝ) : bernoulliAverage p f = ((1 - p) * bernoulliAverage p fun (x : Fin n → Bool) => f (Fin.cons false x)) + p * bernoulliAverage p fun (x : Fin n → Bool) => f (Fin.cons true x)

theorem Complexity.BooleanAnalysis.bernoulliAverage_mono_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) {f g : (ι → Bool) → ℝ} (hfg : ∀ (x : ι → Bool), f x ≤ g x) : bernoulliAverage p f ≤ bernoulliAverage p g

theorem Complexity.BooleanAnalysis.bernoulliAverage_const_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p c : ℝ) : (bernoulliAverage p fun (x : ι → Bool) => c) = c

theorem Complexity.BooleanAnalysis.bernoulliWeight_reindex_internal {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p : ℝ) (s : κ → Bool) : (bernoulliWeight p fun (i : ι) => s (e i)) = bernoulliWeight p s

theorem Complexity.BooleanAnalysis.bernoulliAverage_reindex_internal {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (p : ℝ) (f : (κ → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f fun (j : κ) => x (e.symm j)) = bernoulliAverage p f

theorem Complexity.BooleanAnalysis.bernoulliWeight_split_internal {ι : Type u_1} [Fintype ι] (p : ℝ) (s x : ι → Bool) : bernoulliWeight p x = (bernoulliWeight p fun (i : { i : ι // s i = true }) => x ↑i) * bernoulliWeight p fun (i : { i : ι // s i ≠ true }) => x ↑i

theorem Complexity.BooleanAnalysis.bernoulliAverage_restrict_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (s : ι → Bool) (f : ({ i : ι // s i = true } → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f fun (i : { i : ι // s i = true }) => x ↑i) = bernoulliAverage p f

theorem Complexity.BooleanAnalysis.bernoulliAverage_linear_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p a b : ℝ) (f g : (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => a * f x + b * g x) = a * bernoulliAverage p f + b * bernoulliAverage p g

theorem Complexity.BooleanAnalysis.bernoulliAverage_bias_antitone_internal {n : ℕ} {f : (Fin n → Bool) → ℝ} (hf : Antitone f) {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) (hq : q ≤ 1) : bernoulliAverage q f ≤ bernoulliAverage p f

theorem Complexity.BooleanAnalysis.bernoulliAverage_union_internal {n : ℕ} (p q : ℝ) (f : (Fin n → Bool) → ℝ) : (bernoulliAverage p fun (r : Fin n → Bool) => bernoulliAverage q fun (s : Fin n → Bool) => f fun (i : Fin n) => r i || s i) = bernoulliAverage (p + q - p * q) f

theorem Complexity.BooleanAnalysis.bernoulliAverage_mul_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p a : ℝ) (f : (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => a * f x) = a * bernoulliAverage p f

theorem Complexity.BooleanAnalysis.bernoulliAverage_indicator_bounds_internal {n : ℕ} (A : Set (Fin n → Bool)) {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) : (0 ≤ bernoulliAverage p fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ∧ (bernoulliAverage p fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ≤ 1

theorem Complexity.BooleanAnalysis.lowerSet_indicator_antitone_internal {n : ℕ} {A : Set (Fin n → Bool)} (hA : IsLowerSet A) : Antitone fun (x : Fin n → Bool) => if x ∈ A then 1 else 0

theorem Complexity.BooleanAnalysis.bernoulliAverage_lowerSet_union_internal {n : ℕ} {A : Set (Fin n → Bool)} (hA : IsLowerSet A) {p q : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hq : 0 ≤ q) (hq' : q ≤ 1) : (bernoulliAverage (p + q - p * q) fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ≤ (bernoulliAverage p fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) * bernoulliAverage q fun (x : Fin n → Bool) => if x ∈ A then 1 else 0

theorem Complexity.BooleanAnalysis.bernoulliAverage_lowerSet_pow_le_internal {n : ℕ} {A : Set (Fin n → Bool)} (hA : IsLowerSet A) {p q : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hq : q ≤ 1) (h : ℕ) (hh : ↑h * p ≤ q) : (bernoulliAverage q fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ≤ (bernoulliAverage p fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ^ h

theorem Complexity.BooleanAnalysis.bernoulliAverage_zero_internal {n : ℕ} (f : (Fin n → Bool) → ℝ) : bernoulliAverage 0 f = f fun (x : Fin n) => false

theorem Complexity.BooleanAnalysis.bernoulliAverage_lowerSet_transfer_internal {n : ℕ} {A : Set (Fin n → Bool)} (hA : IsLowerSet A) (hA' : A.Nonempty) {r : ℝ} (hr : 0 ≤ r) (hr' : r ≤ 1 / 20) : (bernoulliAverage (1 / 4) fun (x : Fin n → Bool) => if x ∈ A then 1 else 0) ^ (5 * r) ≤ bernoulliAverage r fun (x : Fin n → Bool) => if x ∈ A then 1 else 0

theorem Complexity.BooleanAnalysis.bernoulliAverage_expect_comm_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} (A : Finset α) (p : ℝ) (f : (ι → Bool) → α → ℝ) : (bernoulliAverage p fun (s : ι → Bool) => A.expect fun (x : α) => f s x) = A.expect fun (x : α) => bernoulliAverage p fun (s : ι → Bool) => f s x

theorem Complexity.BooleanAnalysis.bernoulliAverage_sub_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f g : (ι → Bool) → ℝ) : (bernoulliAverage p fun (s : ι → Bool) => f s - g s) = bernoulliAverage p f - bernoulliAverage p g