Joint sampling of a union and a difference

Finite product proof of the conditional sampling law used in the mirror-set argument of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

The algebraic law is stated with (p + q - p*q)*r = p*(1-q), so it also covers degenerate rates. The subtype version samples only inside the union.

theorem Complexity.BooleanAnalysis.bernoulliAverage_union_difference_fin_internal {n : ℕ} (p q r : ℝ) (hr : (p + q - p * q) * r = p * (1 - q)) (f : (Fin n → Bool) → (Fin n → Bool) → ℝ) : (bernoulliAverage p fun (P : Fin n → Bool) => bernoulliAverage q fun (Q : Fin n → Bool) => f (fun (i : Fin n) => P i || Q i) fun (i : Fin n) => P i && !Q i) = bernoulliAverage (p + q - p * q) fun (S : Fin n → Bool) => bernoulliAverage r fun (T : Fin n → Bool) => f S fun (i : Fin n) => S i && T i

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

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

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