Weighted counts of independent events

The computations with weighted counts (DescriptiveComplexity.weightedCount) that make a query safe: its weighted count, a sum over exponentially many valuations, is a product and a sum over the variables.

• DescriptiveComplexity.weightedCount_forall: an event that constrains each variable separately has a product as weighted count.
• DescriptiveComplexity.weightedCount_sum_type: conditioning on the values of one group of variables.
• DescriptiveComplexity.weightedCount_add_not: an event and its complement share the total weight.
• DescriptiveComplexity.prod_add_eq_prod_add_sum: the first success identity. With F i the weight of a failure at i and S i that of a success, the total weight ∏ (F i + S i) is the weight ∏ F i of failing everywhere, plus, for each i, the weight of failing before i, succeeding at i, and doing anything after. It turns the difference ∏ (F i + S i) - ∏ F i, the weight of succeeding somewhere, into a sum of products: no subtraction is left, which is what a quantitative term needs.

theorem DescriptiveComplexity.weightedCount_add_not {X : Type} [Fintype X] [DecidableEq X] (a c : X → ℕ) (f : (X → Bool) → Bool) : (weightedCount a c f + weightedCount a c fun (v : X → Bool) => !f v) = ∏ x : X, (a x + c x)

An event and its complement share the total weight.

theorem DescriptiveComplexity.weightedCount_forall {X : Type} [Fintype X] [DecidableEq X] (a c : X → ℕ) (ok : X → Bool → Bool) : (weightedCount a c fun (v : X → Bool) => decide (∀ (x : X), ok x (v x) = true)) = ∏ x : X, ((if ok x true = true then a x else 0) + if ok x false = true then c x else 0)

An event constraining each variable separately: its weighted count is the product, over the variables, of the weights of the values it allows.

theorem DescriptiveComplexity.weightedCount_sum_type {X : Type} [Fintype X] [DecidableEq X] (a c : X → ℕ) {Y : Type} [Fintype Y] [DecidableEq Y] (a' c' : Y → ℕ) (f : (X ⊕ Y → Bool) → Bool) : weightedCount (Sum.elim a a') (Sum.elim c c') f = ∑ vX : X → Bool, valWeight a c vX * weightedCount a' c' fun (vY : Y → Bool) => f (Sum.elim vX vY)

Conditioning on a group of variables: the weighted count over two groups is the sum, over the valuations of the first, of their weight times the weighted count over the second.

First success

theorem DescriptiveComplexity.prod_add_eq_prod_add_sum {I : Type} [Fintype I] [LinearOrder I] (F S : I → ℕ) : ∏ i : I, (F i + S i) = ∏ i : I, F i + ∑ i : I, (∏ j : I with j < i, F j) * S i * ∏ j : I with i < j, (F j + S j)

The first success identity: the total weight is the weight of failing everywhere, plus the weights of failing before an index, succeeding at it, and doing anything after.