36 Boolean Analysis — Bernoulli Restriction

36.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.

36.2 Declarations

Definition 36.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 36.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 36.3 Nonnegativity of Bernoulli weights

✓

If \(0 \le p \le 1\), then for every restriction \(\rho \) the weight \(\mathrm{bernoulliRestrWeight}(p,\rho )\) is nonnegative.

Lemma 36.4 Bernoulli weights sum to one

✓

If \(0 \le p \le 1\), then the Bernoulli weights form a probability distribution: summing \(\mathrm{bernoulliRestrWeight}(p,\rho )\) over all restrictions \(\rho \) on \(n\) variables yields \(1\).

Lemma 36.5 Bernoulli event probability is at most one

✓

If \(0 \le p \le 1\), then for every (decidable) event the Bernoulli probability \(\mathrm{bernoulliRestrProb}(p,\mathrm{event})\) is at most \(1\).