Independent Boolean variables: probabilities, and weighted counts

The concrete side of probabilistic query evaluation, with no logic in it: a finite set X of independent Boolean variables – the uncertain facts of a tuple-independent database – each true with its own rational probability.

The first part is taken from the library provenance-lean (Provenance.Probability), where it underlies the probabilistic semantics of ProvSQL: DescriptiveComplexity.ProbAssignment, the probability DescriptiveComplexity.ProbAssignment.valProb of a valuation (a possible world), the fact that these form a distribution (DescriptiveComplexity.ProbAssignment.sum_valProb_eq_one), and the probability DescriptiveComplexity.ProbAssignment.funcProb of an event.

The second part is what the counting side needs. A probability a / (a + c) is a pair of natural weights, a for “true” and c for “false” (DescriptiveComplexity.ProbAssignment.ofWeights). The weighted count of an event (DescriptiveComplexity.weightedCount) is the sum, over the valuations in it, of the product of the weights each variable takes. Then

Pr(f) = weightedCount f / weightedCount ⊤

(DescriptiveComplexity.ProbAssignment.funcProb_ofWeights): a probability is a ratio of two weighted counts, and those are natural numbers.

structure DescriptiveComplexity.ProbAssignment (X : Type) : Type

A probability assignment to a finite set X of Boolean variables: each variable is assigned a rational probability in [0, 1].

• prob : X → ℚ

  The probability assigned to each variable.

• prob_nonneg (x : X) : 0 ≤ self.prob x

  Probabilities are non-negative.

• prob_le_one (x : X) : self.prob x ≤ 1

  Probabilities are at most 1.

def DescriptiveComplexity.ProbAssignment.valProb {X : Type} [Fintype X] (P : ProbAssignment X) (v : X → Bool) : ℚ

Probability of a single valuation v : X → Bool, under the independence assumption: Pr(v) = ∏_{v(x)=⊤} Pr(x) · ∏_{v(x)=⊥} (1 - Pr(x)).

Equations

• P.valProb v = ∏ x : X, if v x = true then P.prob x else 1 - P.prob x

theorem DescriptiveComplexity.ProbAssignment.valProb_nonneg {X : Type} [Fintype X] (P : ProbAssignment X) (v : X → Bool) : 0 ≤ P.valProb v

theorem DescriptiveComplexity.ProbAssignment.valProb_le_one {X : Type} [Fintype X] (P : ProbAssignment X) (v : X → Bool) : P.valProb v ≤ 1

theorem DescriptiveComplexity.ProbAssignment.sum_valProb_eq_one {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) : ∑ v : X → Bool, P.valProb v = 1

The valuations form a probability distribution: ∑ v, Pr(v) = 1.

def DescriptiveComplexity.ProbAssignment.funcProb {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) (f : (X → Bool) → Bool) : ℚ

Probability of an event, a Boolean function of the valuation: Pr(f) = ∑_{v ⊨ f} Pr(v).

Equations

• P.funcProb f = ∑ v : X → Bool, if f v = true then P.valProb v else 0

Weights

def DescriptiveComplexity.valWeight {X : Type} [Fintype X] (a c : X → ℕ) (v : X → Bool) : ℕ

The weight of a valuation: the product, over the variables, of the weight a of those it makes true and the weight c of those it makes false.

Equations

• DescriptiveComplexity.valWeight a c v = ∏ x : X, if v x = true then a x else c x

def DescriptiveComplexity.weightedCount {X : Type} [Fintype X] [DecidableEq X] (a c : X → ℕ) (f : (X → Bool) → Bool) : ℕ

The weighted count of an event: the sum of the weights of the valuations in it.

Equations

• DescriptiveComplexity.weightedCount a c f = ∑ v : X → Bool, if f v = true then DescriptiveComplexity.valWeight a c v else 0

def DescriptiveComplexity.ProbAssignment.ofWeights {X : Type} (a c : X → ℕ) (h : ∀ (x : X), 0 < a x + c x) : ProbAssignment X

The probability assignment of a family of weights: the variable x is true with probability a x / (a x + c x).

Equations

• DescriptiveComplexity.ProbAssignment.ofWeights a c h = { prob := fun (x : X) => ↑(a x) / (↑(a x) + ↑(c x)), prob_nonneg := ⋯, prob_le_one := ⋯ }

theorem DescriptiveComplexity.ProbAssignment.valProb_ofWeights {X : Type} [Fintype X] {a c : X → ℕ} (h : ∀ (x : X), 0 < a x + c x) (v : X → Bool) : (ofWeights a c h).valProb v = ↑(valWeight a c v) / ↑(∏ x : X, (a x + c x))

The probability of a valuation is its weight, over the product of the total weights.

theorem DescriptiveComplexity.ProbAssignment.funcProb_ofWeights {X : Type} [Fintype X] [DecidableEq X] {a c : X → ℕ} (h : ∀ (x : X), 0 < a x + c x) (f : (X → Bool) → Bool) : (ofWeights a c h).funcProb f = ↑(weightedCount a c f) / ↑(weightedCount a c fun (x : X → Bool) => true)

A probability is a ratio of two weighted counts: the probability of an event is its weighted count, divided by the weighted count of the sure event.