Bernoulli coordinate sampling and transference

Boolean masks represent subsets of coordinates, ordered by inclusion. Increasing the sampling rate decreases expectations of antitone functions. Unions of independently sampled masks yield the downward-closed transference 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 attributes this principle to Yufei Zhao, Probabilistic Methods in Combinatorics, Lemma 4.3.7.

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

Product Bernoulli weights sum to one. This identity holds algebraically for every p; they are nonnegative when p ∈ [0, 1].

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

Bernoulli expectation preserves pointwise inequalities at probability rates.

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

An equivalence of coordinate types preserves Bernoulli expectations.

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

Restricting a Bernoulli mask to fixed coordinates preserves its product law.

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

Sampling at rate zero selects the empty coordinate set.

theorem Complexity.BooleanAnalysis.bernoulliAverage_bias_antitone {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

Increasing the sampling rate decreases the expectation of an antitone function.

theorem Complexity.BooleanAnalysis.bernoulliAverage_union {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

The union of independent masks of rates p and q has rate p + q - p * q.

theorem Complexity.BooleanAnalysis.bernoulliAverage_lowerSet_pow_le {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

Integer repetition form of downward-closed transference. If h independent rate-p masks have union rate at most q, membership at rate q forces every mask to belong to the downward-closed family. The hypothesis h * p ≤ q bounds that union rate. No nonemptiness assumption is needed.

theorem Complexity.BooleanAnalysis.bernoulliAverage_lowerSet_transfer {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

The 1/4-to-sparse transfer inequality used in Korten's Lemma 10. Nonemptiness covers the endpoint r = 0, where the right side is one.