Conditional sampling inside a union of masks

Let P and Q be independent random masks of rates p and q. Their union S has rate p + q - p q, and conditionally on S, the difference P \ Q selects each coordinate of S independently with rate conditionalSamplingRate p q = p (1 - q) / (p + q - p q) (bernoulliAverage_union_difference). The law is stated as an equality of finite expectations for any rate r with (p + q - p q) r = p (1 - q), so it avoids conditioning on events of probability zero and covers degenerate rates. This is the coordinate-sampling step of Korten's proof of the mirror-set lemma [Kor26].

Main definitions

• Cslib.BitString.conditionalSamplingRate: the conditional rate of P \ Q inside P ∪ Q.

Main results

• Cslib.BitString.bernoulliAverage_union_difference: the joint law of P ∪ Q and P \ Q.
• Cslib.BitString.bernoulliAverage_union_difference_subtype: the same, with the difference as a mask on the coordinates of the union.
• Cslib.BitString.conditionalSamplingRate_nonneg, Cslib.BitString.conditionalSamplingRate_le_one, Cslib.BitString.conditionalSamplingRate_le_div: the conditional rate is a probability, at most p / q.

References

• O. Korten, Top-Down Lower Bounds for All Depths

noncomputable def Cslib.BitString.conditionalSamplingRate (p q : ℝ) : ℝ

The rate p (1 - q) / (p + q - p q) at which the difference P \ Q of independent masks of rates p and q selects the coordinates of their union P ∪ Q.

theorem Cslib.BitString.mul_conditionalSamplingRate {p q : ℝ} (h : p + q - p * q ≠ 0) : (p + q - p * q) * conditionalSamplingRate p q = p * (1 - q)

The conditional rate solves (p + q - p q) r = p (1 - q) when the union has positive rate.

theorem Cslib.BitString.conditionalSamplingRate_nonneg {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hq' : q ≤ 1) : 0 ≤ conditionalSamplingRate p q

For p ≥ 0 and 0 ≤ q ≤ 1, the conditional rate is nonnegative.

theorem Cslib.BitString.conditionalSamplingRate_le_one {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) (hq' : q ≤ 1) : conditionalSamplingRate p q ≤ 1

For p ≥ 0 and 0 < q ≤ 1, the conditional rate is at most one.

theorem Cslib.BitString.conditionalSamplingRate_le_div {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) (hq' : q ≤ 1) : conditionalSamplingRate p q ≤ p / q

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

theorem Cslib.BitString.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

The joint law of P ∪ Q and P \ Q: for independent masks P and Q of rates p and q, the union and the difference are distributed as a mask S of rate p + q - p q and the part inside S of an independent mask of rate r, when (p + q - p q) r = p (1 - q).

theorem Cslib.BitString.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)

The joint law of P ∪ Q and P \ Q, with the difference as a mask on the coordinates of the union.