TCSLib

32 Boolean Analysis — Restriction Compose

32.1 Overview

This module shows that Bernoulli random restrictions compose: applying a Bernoulli(\(p\)) restriction and then a Bernoulli(\(q\)) restriction on the remaining free variables yields the same distribution as a single Bernoulli(\(pq\)) restriction. It introduces the composition of two restrictions and the per-variable weight, and builds up through factorization and fiber-weight identities to the main composition equality and its probabilistic inequality corollary.

32.2 Declarations

Definition 32.1 Composition of two restrictions
#

Given two restrictions \(\rho _1, \rho _2\) on \(n\) variables, their composition is the restriction that on each coordinate \(i\) uses the value fixed by \(\rho _1\) if there is one, and otherwise the value given by \(\rho _2\). This models applying \(\rho _1\) first and then \(\rho _2\) on the variables left free by \(\rho _1\).

Definition 32.2 Per-variable Bernoulli weight
#

For a parameter \(p \in \mathbb {R}\), the per-variable weight assigns \(p\) to a free coordinate (value none) and \((1-p)/2\) to a fixed coordinate (value some_), matching the marginal of the Bernoulli restriction model.

Lemma 32.3 Pointwise characterization of composition
#

The composition \(\mathrm{composeRestr}\, \rho _1\, \rho _2\) equals \(\sigma \) if and only if for every coordinate \(i\) the value \((\rho _1\, i)\), falling back to \((\rho _2\, i)\), equals \(\sigma \, i\).

Lemma 32.4 Right identity for composition

Composing a restriction \(\rho \) with the all-free restriction (which fixes no variable) returns \(\rho \) unchanged.

Lemma 32.5 Bernoulli weight factors as a product

The Bernoulli restriction weight of \(\rho \) at parameter \(p\) equals the product over all coordinates \(i\) of the per-variable weights:

\[ \mathrm{bernoulliRestrWeight}\, p\, \rho = \prod _{i : \mathrm{Fin}\, n} \mathrm{varWeight}\, p\, (\rho \, i). \]
Lemma 32.6 Per-variable composition identity
#

For parameters \(p, q \in \mathbb {R}\) and any outcome \(c\), summing the products \(\mathrm{varWeight}\, p\, a \cdot \mathrm{varWeight}\, q\, b\) over all pairs \((a,b)\) whose composition equals \(c\) gives \(\mathrm{varWeight}\, (pq)\, c\):

\[ \sum _{a} \sum _{b} \mathrm{varWeight}\, p\, a \cdot \mathrm{varWeight}\, q\, b \cdot [\, a \, \triangleright \, b = c\, ] = \mathrm{varWeight}\, (pq)\, c. \]
Lemma 32.7 Fiber weight identity

Summing the product \(\mathrm{bernoulliRestrWeight}\, p\, \rho _1 \cdot \mathrm{bernoulliRestrWeight}\, q\, \rho _2\) over all pairs \((\rho _1, \rho _2)\) that compose to \(\sigma \) equals the Bernoulli weight of \(\sigma \) at parameter \(pq\):

\[ \sum _{\rho _1}\sum _{\rho _2} \mathrm{bernoulliRestrWeight}\, p\, \rho _1 \cdot \mathrm{bernoulliRestrWeight}\, q\, \rho _2 \cdot [\, \mathrm{composeRestr}\, \rho _1\, \rho _2 = \sigma \, ] = \mathrm{bernoulliRestrWeight}\, (pq)\, \sigma . \]
Theorem 32.8 Composition of Bernoulli random restrictions, equality

For \(0 \lt p \le 1\), \(0 \lt q \le 1\) and any event on restrictions, the Bernoulli(\(pq\)) probability of the event equals the weighted average, over Bernoulli(\(p\)) restrictions \(\rho _1\), of the Bernoulli(\(q\)) probability that the event holds after composing with \(\rho _1\):

\[ \mathrm{bernoulliRestrProb}\, (pq)\, \mathrm{event} = \sum _{\rho _1} \mathrm{bernoulliRestrWeight}\, p\, \rho _1 \cdot \mathrm{bernoulliRestrProb}\, q\, \bigl(\rho _2 \mapsto \mathrm{event}(\mathrm{composeRestr}\, \rho _1\, \rho _2)\bigr). \]

This says a Bernoulli(\(p\)) restriction followed by a Bernoulli(\(q\)) restriction on the remaining free variables has the same distribution as a single Bernoulli(\(pq\)) restriction.

Theorem 32.9 Composition inequality

For \(0 \lt p \le 1\) and \(0 \lt q \le 1\), the Bernoulli(\(pq\)) probability of an event is at most the Bernoulli(\(p\)) probability that some \(\rho _2\) makes the event hold after composition:

\[ \mathrm{bernoulliRestrProb}\, (pq)\, \mathrm{event} \le \mathrm{bernoulliRestrProb}\, p\, \bigl(\rho _1 \mapsto \exists \rho _2,\; \mathrm{event}(\mathrm{composeRestr}\, \rho _1\, \rho _2)\bigr). \]