Conditional sampling inside a coordinate union

Let P and Q be independent Bernoulli masks with rates p and q. Their union has rate p + q - p*q. Conditional on that union S, the mask P \ Q has independent coordinates inside S, with rate r = p*(1-q)/(p+q-p*q). The theorems express this law as equality of finite expectations, avoiding conditioning on zero-probability events.

This is the coordinate-sampling step in Oliver Korten's mirror-set proof, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

theorem Complexity.BooleanAnalysis.bernoulliAverage_union_difference {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q r : ℝ) (hr : (p + q - p * q) * r = p * (1 - q)) (f : (ι → Bool) → (ι → Bool) → ℝ) : (bernoulliAverage p fun (P : ι → Bool) => bernoulliAverage q fun (Q : ι → Bool) => f (fun (i : ι) => P i || Q i) fun (i : ι) => P i && !Q i) = bernoulliAverage (p + q - p * q) fun (S : ι → Bool) => bernoulliAverage r fun (T : ι → Bool) => f S fun (i : ι) => S i && T i

Joint law of P ∪ Q and P \ Q, with the difference represented as a mask on the full coordinate set. The product identity includes degenerate rates.

theorem Complexity.BooleanAnalysis.bernoulliAverage_union_difference_subtype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q r : ℝ) (hr : (p + q - p * q) * r = p * (1 - q)) (f : (S : ι → Bool) → ({ i : ι // S i = true } → Bool) → ℝ) : (bernoulliAverage p fun (P : ι → Bool) => bernoulliAverage q fun (Q : ι → Bool) => f (fun (i : ι) => P i || Q i) fun (i : { i : ι // (P i || Q i) = true }) => P ↑i && !Q ↑i) = bernoulliAverage (p + q - p * q) fun (S : ι → Bool) => bernoulliAverage r (f S)

Conditional product law on the selected-coordinate subtype. The test function may depend on the union and its smaller coordinate type.

theorem Complexity.BooleanAnalysis.conditionalSamplingRate_bounds {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) (hq' : q ≤ 1) : 0 ≤ p * (1 - q) / (p + q - p * q) ∧ p * (1 - q) / (p + q - p * q) ≤ p / q ∧ p * (1 - q) / (p + q - p * q) ≤ 1

For p ≥ 0 and 0 < q ≤ 1, the conditional difference rate is a probability and is at most p/q.