33 Boolean Analysis — Bernoulli Restriction

33.1 Overview

This module sets up the Bernoulli probability model for random restrictions, in which each of the \(n\) variables is independently left free with probability \(p\) and fixed to \(\mathsf{true}\) or \(\mathsf{false}\) each with probability \((1-p)/2\). It defines the weight of a single restriction and the probability of an event, and records the basic facts that the weights are nonnegative, sum to one, and that every event probability is at most one.

33.2 Declarations

Definition 33.1 Bernoulli weight of a restriction

✓

For a parameter \(p \in \mathbb {R}\) and a restriction \(\rho \) on \(n\) variables, the Bernoulli weight is

\[ p^{\left\lvert \mathrm{freeVars}(\rho )\right\rvert } \cdot \left(\tfrac {1-p}{2}\right)^{\, n - \left\lvert \mathrm{freeVars}(\rho )\right\rvert }, \]

so each free variable contributes a factor \(p\) and each fixed variable a factor \((1-p)/2\).

Definition 33.2 Bernoulli event probability

✓

For a parameter \(p\) and a (decidable) predicate \(\mathrm{event}\) on restrictions, the probability that the predicate holds under a Bernoulli(\(p\)) random restriction is the sum over all restrictions \(\rho \) of \(\mathrm{bernoulliRestrWeight}(p,\rho )\) weighted by the indicator of \(\mathrm{event}(\rho )\).

Lemma 33.3 Nonnegativity of the Bernoulli weight

✓

Let \(p \in \mathbb {R}\) satisfy \(0 \le p \le 1\), and let \(\rho \) be a restriction on \(n\) variables, with \(f\) of its variables left free. Then its Bernoulli weight \(p^{f}\, \bigl(\tfrac {1-p}{2}\bigr)^{\, n - f}\) is nonnegative.

Lemma 33.4 Bernoulli restriction weights sum to one

✓

Fix \(n \in \mathbb {N}\) and a real parameter \(p\) with \(0 \le p \le 1\). For a restriction \(\rho \) on \(n\) variables, write \(F(\rho )\) for its set of free variables. Then, summing the Bernoulli weight over all restrictions,

\[ \sum _{\rho } p^{\left\lvert F(\rho )\right\rvert } \left(\tfrac {1-p}{2}\right)^{\, n - \left\lvert F(\rho )\right\rvert } = 1, \]

so these weights define a probability distribution on the set of restrictions on \(n\) variables.

Lemma 33.5 Bernoulli restriction probability is at most one

✓

Fix \(n\) and a real parameter \(p\) with \(0 \le p \le 1\). Then for every decidable predicate on restrictions of \(n\) variables, the probability that it holds under a Bernoulli(\(p\)) random restriction is at most \(1\).