Probability identities for HAVING aggregate comparisons under independence

This file formalizes the algebraic identities for evaluating HAVING-style aggregate comparisons when the contributors are independent. Given a B[X]-instance in which each contributor i : ι carries an annotation α i : BoolFunc X and the annotations have pairwise disjoint variable supports (so the contributors are independent Bernoullis with marginals p i = P.funcProb (α i)), we give closed-form / recurrence expressions for the probability that the aggregate-comparison atom holds on the contributors of a single group:

• MAX / MIN factorization (funcProb_maxLeOnNonempty, funcProb_minGeOnNonempty): Pr[max ≤ C on nonempty] = (∏_{t i > C}(1 - p i)) · (1 - ∏_{t i ≤ C}(1 - p i)) and the dual for min.
• COUNT (Poisson-binomial) recurrence (countMass_insert_succ, countMass_insert_zero): ρ_{J ⊔ {i}}(j+1) = (1 - p i) · ρ_J(j+1) + p i · ρ_J(j), ρ_{J ⊔ {i}}(0) = (1 - p i) · ρ_J(0).
• SUM (weighted Poisson-binomial) recurrence (sumMass_insert): σ_{J ⊔ {i}}(s) = (1 - p i) · σ_J(s) + p i · σ_J(s - t i) (with the convention that σ_J at a negative-shifted index is 0).

All four results follow the same template: the underlying event factors as a Boolean combination of the per-contributor indicators, and the disjoint-supports hypothesis turns that combination into a product of marginal probabilities via ProbAssignment.funcProb_mul_disjoint.

theorem BoolFunc.DependsOn.zero {X : Type} {S : Finset X} : DependsOn 0 S

The constant 0 Boolean function depends on the empty support (equivalently on any support).

theorem BoolFunc.DependsOn.one {X : Type} {S : Finset X} : DependsOn 1 S

The constant 1 Boolean function depends on the empty support (equivalently on any support).

theorem BoolFunc.DependsOn.var {X : Type} [DecidableEq X] (i : X) : (BoolFunc.var i).DependsOn {i}

A variable depends on the singleton of its index.

theorem BoolFunc.DependsOn.mul {X : Type} [DecidableEq X] {f g : BoolFunc X} {S T : Finset X} (hf : f.DependsOn S) (hg : g.DependsOn T) : (f * g).DependsOn (S ∪ T)

f * g depends on S ∪ T whenever f depends on S and g on T. Multiplication in BoolFunc X is pointwise &&.

theorem BoolFunc.DependsOn.add {X : Type} [DecidableEq X] {f g : BoolFunc X} {S T : Finset X} (hf : f.DependsOn S) (hg : g.DependsOn T) : (f + g).DependsOn (S ∪ T)

f + g depends on S ∪ T. Addition in BoolFunc X is pointwise ||.

theorem BoolFunc.DependsOn.one_sub {X : Type} {f : BoolFunc X} {S : Finset X} (hf : f.DependsOn S) : (1 - f).DependsOn S

1 - f depends on the same support as f. Subtraction here is pointwise (1 v) && !(f v) = !(f v).

theorem BoolFunc.DependsOn.mono {X : Type} {f : BoolFunc X} {S T : Finset X} (hf : f.DependsOn S) (hST : S ⊆ T) : f.DependsOn T

Enlarging the support preserves DependsOn.

theorem BoolFunc.DependsOn.prod {X : Type} [DecidableEq X] {ι : Type} [DecidableEq ι] {β : ι → BoolFunc X} {S : ι → Finset X} (h : ∀ (i : ι), (β i).DependsOn (S i)) (J : Finset ι) : (∏ i ∈ J, β i).DependsOn (J.biUnion S)

Finset.prod of BoolFuncs depends on the biUnion of the per-factor supports.

theorem ProbAssignment.funcProb_prod_disjoint {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) {ι : Type} [DecidableEq ι] (β : ι → BoolFunc X) (S : ι → Finset X) (hdep : ∀ (i : ι), (β i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (J : Finset ι) : P.funcProb (∏ i ∈ J, β i) = ∏ i ∈ J, P.funcProb (β i)

Iterated independence: if (β i) depends on S i and the supports are pairwise disjoint, then the probability of ∏ i ∈ J, β i factors as the product of the marginal probabilities P.funcProb (β i).

theorem ProbAssignment.funcProb_sum_incompatible {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) {ι : Type} [DecidableEq ι] (β : ι → BoolFunc X) (J : Finset ι) (hpair : ∀ i ∈ J, ∀ j ∈ J, i ≠ j → β i * β j = 0) : P.funcProb (∑ i ∈ J, β i) = ∑ i ∈ J, P.funcProb (β i)

Additivity over pairwise-incompatible events: the probability of a ⊕-sum (pointwise OR) of Boolean functions whose pairwise products vanish is the sum of the probabilities.

Common setup for the four results

We fix a probability assignment P over Boolean variables X, a finite type ι of contributors, an annotation α : ι → BoolFunc X, supports S : ι → Finset X that are pairwise disjoint, and a hypothesis hdep : ∀ i, (α i).DependsOn (S i). The contributor marginal is p i := P.funcProb (α i).

theorem HavingProbability.prod_eval_eq_true_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [DecidableEq ι] (J : Finset ι) (β : ι → BoolFunc X) (v : X → Bool) : (∏ i ∈ J, β i) v = true ↔ ∀ i ∈ J, β i v = true

Pointwise evaluation of a Finset product of BoolFuncs: the product evaluates to true iff every factor does.

MAX factorization

def HavingProbability.maxNoneAbove {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world contains no contributor with value > C”: the AND over the indicators 1 - α i for all contributors with t i > C. Evaluates to true iff every such contributor's annotation is false.

Equations

• HavingProbability.maxNoneAbove α t C = ∏ i : ι with C < t i, (1 - α i)

def HavingProbability.someAtMost {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world contains some contributor with value ≤ C”: the OR over the indicators α i for all contributors with t i ≤ C, expressed as 1 - ∏ (1 - α i).

Equations

• HavingProbability.someAtMost α t C = 1 - ∏ i : ι with t i ≤ C, (1 - α i)

def HavingProbability.maxLeOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world is nonempty and max_{i ∈ world} t i ≤ C”: the conjunction of the two pieces above. The semantic meaning is recorded in maxLeOnNonempty_eval_iff.

Equations

• HavingProbability.maxLeOnNonempty α t C = HavingProbability.maxNoneAbove α t C * HavingProbability.someAtMost α t C

theorem HavingProbability.maxNoneAbove_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : maxNoneAbove α t C v = true ↔ ∀ (i : ι), α i v = true → t i ≤ C

Semantic reading of maxNoneAbove.

theorem HavingProbability.someAtMost_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : someAtMost α t C v = true ↔ ∃ (i : ι), t i ≤ C ∧ α i v = true

Semantic reading of someAtMost.

theorem HavingProbability.maxLeOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : maxLeOnNonempty α t C v = true ↔ (∃ (i : ι), α i v = true) ∧ ∀ (i : ι), α i v = true → t i ≤ C

Full semantic reading: the BoolFunc maxLeOnNonempty α t C evaluates to true at v iff the random world {i : α i v = true} is nonempty and its maximum-of-t is at most C.

theorem HavingProbability.funcProb_maxNoneAbove {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (maxNoneAbove α t C) = ∏ i : ι with C < t i, (1 - P.funcProb (α i))

Probability of maxNoneAbove: by iterated independence applied to (1 - α i)'s, this is the product of (1 - p i) over contributors above C.

theorem HavingProbability.funcProb_someAtMost {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (someAtMost α t C) = 1 - ∏ i : ι with t i ≤ C, (1 - P.funcProb (α i))

Probability of someAtMost: the complement of the product.

theorem HavingProbability.funcProb_maxLeOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (maxLeOnNonempty α t C) = (∏ i : ι with C < t i, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with t i ≤ C, (1 - P.funcProb (α i)))

MAX factorization under independence. The probability of the “max ≤ C on a nonempty world” event factors as a product of an “all above-C contributors are absent” term and a “some at-most-C contributor is present” term.

MIN factorization

def HavingProbability.minNoneBelow {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world contains no contributor with value < C”: the AND over the indicators 1 - α i for all contributors with t i < C.

Equations

• HavingProbability.minNoneBelow α t C = ∏ i : ι with t i < C, (1 - α i)

def HavingProbability.someAtLeast {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world contains some contributor with value ≥ C”.

Equations

• HavingProbability.someAtLeast α t C = 1 - ∏ i : ι with C ≤ t i, (1 - α i)

def HavingProbability.minGeOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world is nonempty and min_{i ∈ world} t i ≥ C”.

Equations

• HavingProbability.minGeOnNonempty α t C = HavingProbability.minNoneBelow α t C * HavingProbability.someAtLeast α t C

theorem HavingProbability.minNoneBelow_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : minNoneBelow α t C v = true ↔ ∀ (i : ι), α i v = true → C ≤ t i

theorem HavingProbability.someAtLeast_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : someAtLeast α t C v = true ↔ ∃ (i : ι), C ≤ t i ∧ α i v = true

theorem HavingProbability.minGeOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : minGeOnNonempty α t C v = true ↔ (∃ (i : ι), α i v = true) ∧ ∀ (i : ι), α i v = true → C ≤ t i

theorem HavingProbability.funcProb_minNoneBelow {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (minNoneBelow α t C) = ∏ i : ι with t i < C, (1 - P.funcProb (α i))

theorem HavingProbability.funcProb_someAtLeast {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (someAtLeast α t C) = 1 - ∏ i : ι with C ≤ t i, (1 - P.funcProb (α i))

theorem HavingProbability.funcProb_minGeOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (minGeOnNonempty α t C) = (∏ i : ι with t i < C, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with C ≤ t i, (1 - P.funcProb (α i)))

MIN factorization under independence.

COUNT (Poisson-binomial) recurrence

def HavingProbability.countEqIndicator {X ι : Type} (α : ι → BoolFunc X) (J : Finset ι) (j : ℕ) : BoolFunc X

Indicator BoolFunc: evaluates to true at a valuation v iff exactly j of the indices i ∈ J have α i v = true.

Equations

• HavingProbability.countEqIndicator α J j v = decide ({i ∈ J | α i v = true}.card = j)

theorem HavingProbability.countEqIndicator_dependsOn {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (J : Finset ι) (j : ℕ) : (countEqIndicator α J j).DependsOn (J.biUnion S)

countEqIndicator α J j depends on ⋃ i ∈ J, S i: its value at v only references α i v for i ∈ J.

theorem HavingProbability.countEqIndicator_insert_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {i : ι} {J : Finset ι} (hi : i ∉ J) : countEqIndicator α (insert i J) 0 = (1 - α i) * countEqIndicator α J 0

Decomposition for j = 0: at most 0 of the indices in insert i J have α k v = true iff α i v = false and at most 0 of the indices in J have α k v = true.

theorem HavingProbability.countEqIndicator_insert_succ {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {i : ι} {J : Finset ι} (hi : i ∉ J) (j : ℕ) : countEqIndicator α (insert i J) (j + 1) = α i * countEqIndicator α J j + (1 - α i) * countEqIndicator α J (j + 1)

Decomposition for j = j' + 1: exactly j' + 1 indices in insert i J have α k v = true iff either α i v = true and exactly j' indices in J do, or α i v = false and exactly j' + 1 indices in J do.

theorem HavingProbability.countMass_insert_succ {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) {i : ι} {J : Finset ι} (hi : i ∉ J) (j : ℕ) : P.funcProb (countEqIndicator α (insert i J) (j + 1)) = (1 - P.funcProb (α i)) * P.funcProb (countEqIndicator α J (j + 1)) + P.funcProb (α i) * P.funcProb (countEqIndicator α J j)

COUNT Poisson-binomial recurrence (succ case). For i ∉ J and j : ℕ, the probability that exactly j + 1 of the contributors in insert i J are present factors as (1 − p i) · ρ_J(j+1) + p i · ρ_J(j).

theorem HavingProbability.countMass_insert_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) {i : ι} {J : Finset ι} (hi : i ∉ J) : P.funcProb (countEqIndicator α (insert i J) 0) = (1 - P.funcProb (α i)) * P.funcProb (countEqIndicator α J 0)

COUNT Poisson-binomial recurrence (zero case). For i ∉ J, the probability that exactly 0 contributors in insert i J are present is (1 − p i) · ρ_J(0).

SUM (weighted Poisson-binomial) recurrence

def HavingProbability.sumEqIndicator {X ι : Type} (α : ι → BoolFunc X) (t : ι → ℕ) (J : Finset ι) (s : ℕ) : BoolFunc X

Indicator BoolFunc: evaluates to true at a valuation v iff the sum of t i over indices i ∈ J with α i v = true equals s.

Equations

• HavingProbability.sumEqIndicator α t J s v = decide ({i ∈ J | α i v = true}.sum t = s)

theorem HavingProbability.sumEqIndicator_dependsOn {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (t : ι → ℕ) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (J : Finset ι) (s : ℕ) : (sumEqIndicator α t J s).DependsOn (J.biUnion S)

Support lemma for sumEqIndicator.

theorem HavingProbability.sumEqIndicator_insert_of_lt {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (t : ι → ℕ) {i : ι} {J : Finset ι} (hi : i ∉ J) {s : ℕ} (hs : s < t i) : sumEqIndicator α t (insert i J) s = (1 - α i) * sumEqIndicator α t J s

Decomposition when the new contributor's weight exceeds the target: if t i > s, the sum cannot reach s once i is included, so the only way to hit s is to leave i out.

theorem HavingProbability.sumEqIndicator_insert_of_le {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (t : ι → ℕ) {i : ι} {J : Finset ι} (hi : i ∉ J) {s : ℕ} (hs : t i ≤ s) : sumEqIndicator α t (insert i J) s = α i * sumEqIndicator α t J (s - t i) + (1 - α i) * sumEqIndicator α t J s

Decomposition when the new contributor's weight fits: if t i ≤ s, the target sum is reachable either without i (target stays s) or with i (target becomes s − t i on the remaining contributors).

theorem HavingProbability.sumMass_insert_of_le {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (t : ι → ℕ) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) {i : ι} {J : Finset ι} (hi : i ∉ J) {s : ℕ} (hs : t i ≤ s) : P.funcProb (sumEqIndicator α t (insert i J) s) = (1 - P.funcProb (α i)) * P.funcProb (sumEqIndicator α t J s) + P.funcProb (α i) * P.funcProb (sumEqIndicator α t J (s - t i))

SUM weighted Poisson-binomial recurrence (weight fits). For i ∉ J and t i ≤ s, the probability that the weighted sum over insert i J equals s factors as (1 − p i) · σ_J(s) + p i · σ_J(s − t i).

theorem HavingProbability.sumMass_insert_of_lt {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (t : ι → ℕ) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) {i : ι} {J : Finset ι} (hi : i ∉ J) {s : ℕ} (hs : s < t i) : P.funcProb (sumEqIndicator α t (insert i J) s) = (1 - P.funcProb (α i)) * P.funcProb (sumEqIndicator α t J s)

SUM weighted Poisson-binomial recurrence (weight too large). For i ∉ J and s < t i, the probability collapses to the keep-out branch: σ_{insert i J}(s) = (1 − p i) · σ_J(s).

The remaining MIN / MAX comparison operators

funcProb_maxLeOnNonempty and funcProb_minGeOnNonempty treat MAX ≤ C and MIN ≥ C. The remaining comparisons all follow from two generic events: guardedSome r q – “no present contributor satisfies r, and some present contributor satisfies q” – and its unguarded special case someOf q. Under the disjoint-supports hypothesis, their probabilities factor exactly as before, and each remaining comparison is an instance:

• MAX < C – guard r i := C ≤ t i, witness q i := t i < C;
• MAX = C – guard r i := C < t i, witness q i := t i = C;
• MAX ≥ C / MAX > C – unguarded witness q i := C ≤ t i / C < t i (non-emptiness is implied by the witness);
• MAX ≠ C on non-empty worlds – the disjoint union of MAX < C and MAX > C, whose probabilities add;

and dually for MIN.

theorem HavingProbability.one_sub_eval {X : Type} [Fintype X] [DecidableEq X] (f : BoolFunc X) (v : X → Bool) : (1 - f) v = !f v

Pointwise evaluation of 1 - f: Boolean negation.

def HavingProbability.noneOf {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) (r : ι → Prop) [DecidablePred r] : BoolFunc X

“No present contributor satisfies r”: AND of the negated indicators over the contributors satisfying r.

Equations

• HavingProbability.noneOf α r = ∏ i : ι with r i, (1 - α i)

def HavingProbability.someOf {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) (q : ι → Prop) [DecidablePred q] : BoolFunc X

“Some present contributor satisfies q”: OR of the indicators over the contributors satisfying q, expressed as 1 - ∏ (1 - α i).

Equations

• HavingProbability.someOf α q = 1 - ∏ i : ι with q i, (1 - α i)

def HavingProbability.guardedSome {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) (r q : ι → Prop) [DecidablePred r] [DecidablePred q] : BoolFunc X

“No present contributor satisfies r, and some present contributor satisfies q”. Every MIN/MAX aggregate comparison on non-empty random worlds is an instance of this event.

Equations

• HavingProbability.guardedSome α r q = HavingProbability.noneOf α r * HavingProbability.someOf α q

theorem HavingProbability.noneOf_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (r : ι → Prop) [DecidablePred r] (v : X → Bool) : noneOf α r v = true ↔ ∀ (i : ι), r i → α i v = false

Semantic reading of noneOf.

theorem HavingProbability.someOf_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (q : ι → Prop) [DecidablePred q] (v : X → Bool) : someOf α q v = true ↔ ∃ (i : ι), q i ∧ α i v = true

Semantic reading of someOf.

theorem HavingProbability.guardedSome_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (r q : ι → Prop) [DecidablePred r] [DecidablePred q] (v : X → Bool) : guardedSome α r q v = true ↔ (∀ (i : ι), r i → α i v = false) ∧ ∃ (i : ι), q i ∧ α i v = true

Semantic reading of guardedSome.

theorem HavingProbability.funcProb_noneOf {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (r : ι → Prop) [DecidablePred r] (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) : P.funcProb (noneOf α r) = ∏ i : ι with r i, (1 - P.funcProb (α i))

Probability of noneOf under independence.

theorem HavingProbability.funcProb_someOf {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (q : ι → Prop) [DecidablePred q] (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) : P.funcProb (someOf α q) = 1 - ∏ i : ι with q i, (1 - P.funcProb (α i))

Probability of someOf under independence.

theorem HavingProbability.funcProb_guardedSome {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (r q : ι → Prop) [DecidablePred r] [DecidablePred q] (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (hrq : ∀ (i : ι), r i → q i → False) : P.funcProb (guardedSome α r q) = (∏ i : ι with r i, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with q i, (1 - P.funcProb (α i)))

Factorization of guardedSome under independence. When the guard r and the witness q are mutually exclusive, the probability of guardedSome r q is the product of an “every r-contributor is absent” term and a “some q-contributor is present” term.

def HavingProbability.maxLtOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MAX(t) < C”.

Equations

• HavingProbability.maxLtOnNonempty α t C = HavingProbability.guardedSome α (fun (i : ι) => C ≤ t i) fun (i : ι) => t i < C

def HavingProbability.maxEqOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MAX(t) = C”.

Equations

• HavingProbability.maxEqOnNonempty α t C = HavingProbability.guardedSome α (fun (i : ι) => C < t i) fun (i : ι) => t i = C

def HavingProbability.someAbove {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world with MAX(t) > C” (such a world is non-empty).

Equations

• HavingProbability.someAbove α t C = HavingProbability.someOf α fun (i : ι) => C < t i

def HavingProbability.someBelow {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Random world with MAX(t) < C” (such a world is non-empty).

Equations

• HavingProbability.someBelow α t C = HavingProbability.someOf α fun (i : ι) => t i < C

def HavingProbability.maxNeOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MAX(t) ≠ C”: disjoint union of MAX < C and MAX > C.

Equations

• HavingProbability.maxNeOnNonempty α t C = HavingProbability.maxLtOnNonempty α t C + HavingProbability.someAbove α t C

def HavingProbability.minGtOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MIN(t) > C”.

Equations

• HavingProbability.minGtOnNonempty α t C = HavingProbability.guardedSome α (fun (i : ι) => t i ≤ C) fun (i : ι) => C < t i

def HavingProbability.minEqOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MIN(t) = C”.

Equations

• HavingProbability.minEqOnNonempty α t C = HavingProbability.guardedSome α (fun (i : ι) => t i < C) fun (i : ι) => t i = C

def HavingProbability.minNeOnNonempty {X ι : Type} [Fintype ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : BoolFunc X

“Non-empty random world with MIN(t) ≠ C”: disjoint union of MIN < C (i.e., some contributor below C is present) and MIN > C.

Equations

• HavingProbability.minNeOnNonempty α t C = HavingProbability.minGtOnNonempty α t C + HavingProbability.someBelow α t C

theorem HavingProbability.maxLtOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : maxLtOnNonempty α t C v = true ↔ (∃ (i : ι), α i v = true) ∧ ∀ (i : ι), α i v = true → t i < C

Semantic reading of maxLtOnNonempty.

theorem HavingProbability.maxEqOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : maxEqOnNonempty α t C v = true ↔ (∀ (i : ι), α i v = true → t i ≤ C) ∧ ∃ (i : ι), t i = C ∧ α i v = true

Semantic reading of maxEqOnNonempty: no present contributor exceeds C and some present contributor attains it.

theorem HavingProbability.minGtOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : minGtOnNonempty α t C v = true ↔ (∃ (i : ι), α i v = true) ∧ ∀ (i : ι), α i v = true → C < t i

Semantic reading of minGtOnNonempty.

theorem HavingProbability.minEqOnNonempty_eval_iff {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) (v : X → Bool) : minEqOnNonempty α t C v = true ↔ (∀ (i : ι), α i v = true → C ≤ t i) ∧ ∃ (i : ι), t i = C ∧ α i v = true

Semantic reading of minEqOnNonempty: no present contributor is below C and some present contributor attains it.

theorem HavingProbability.funcProb_maxLtOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (maxLtOnNonempty α t C) = (∏ i : ι with C ≤ t i, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with t i < C, (1 - P.funcProb (α i)))

MAX < C factorization under independence.

theorem HavingProbability.funcProb_maxEqOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (maxEqOnNonempty α t C) = (∏ i : ι with C < t i, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with t i = C, (1 - P.funcProb (α i)))

MAX = C factorization under independence.

theorem HavingProbability.funcProb_someAbove {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (someAbove α t C) = 1 - ∏ i : ι with C < t i, (1 - P.funcProb (α i))

MAX > C under independence: the complement of “every contributor above C is absent”.

theorem HavingProbability.funcProb_someBelow {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (someBelow α t C) = 1 - ∏ i : ι with t i < C, (1 - P.funcProb (α i))

MIN < C (equivalently MAX-dual) under independence: the complement of “every contributor below C is absent”.

theorem HavingProbability.funcProb_minGtOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (minGtOnNonempty α t C) = (∏ i : ι with t i ≤ C, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with C < t i, (1 - P.funcProb (α i)))

MIN > C factorization under independence.

theorem HavingProbability.funcProb_minEqOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (minEqOnNonempty α t C) = (∏ i : ι with t i < C, (1 - P.funcProb (α i))) * (1 - ∏ i : ι with t i = C, (1 - P.funcProb (α i)))

MIN = C factorization under independence.

theorem HavingProbability.maxLt_mul_someAbove_eq_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : maxLtOnNonempty α t C * someAbove α t C = 0

The events MAX < C (on non-empty worlds) and MAX > C are incompatible: their product is the 𝟘 function.

theorem HavingProbability.minGt_mul_someBelow_eq_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (C : V) : minGtOnNonempty α t C * someBelow α t C = 0

The events MIN > C (on non-empty worlds) and MIN < C are incompatible: their product is the 𝟘 function.

theorem HavingProbability.funcProb_maxNeOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (maxNeOnNonempty α t C) = P.funcProb (maxLtOnNonempty α t C) + P.funcProb (someAbove α t C)

MAX ≠ C on non-empty worlds under independence: probabilities of the two disjoint cases MAX < C and MAX > C add.

theorem HavingProbability.funcProb_minNeOnNonempty {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) {V : Type} [LinearOrder V] (t : ι → V) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (C : V) : P.funcProb (minNeOnNonempty α t C) = P.funcProb (minGtOnNonempty α t C) + P.funcProb (someBelow α t C)

MIN ≠ C on non-empty worlds under independence: probabilities of the two disjoint cases MIN > C and MIN < C add.

CDF assembly for COUNT

The recurrences countMass_insert_zero / countMass_insert_succ compute the point masses ρ_J(j). The results below assemble them into the probability of an arbitrary comparison: the satisfying counts form a subset of {0, …, |J|} (an interval, for the six comparison operators) and the corresponding point masses add; the empty-world mass is ∏ (1 - p i); and the upper tail can be computed as a lower tail of the complemented contributors (Pr[B ≥ C] = Pr[B' ≤ N − C]), which is the shorter of the two summations when C > N/2.

theorem HavingProbability.sum_eval_eq_true_iff {X : Type} [Fintype X] [DecidableEq X] {ι' : Type} [DecidableEq ι'] (J : Finset ι') (β : ι' → BoolFunc X) (v : X → Bool) : (∑ i ∈ J, β i) v = true ↔ ∃ i ∈ J, β i v = true

Pointwise evaluation of a Finset.sum of BoolFuncs: the sum (OR) evaluates to true iff some summand does.

theorem HavingProbability.countEqIndicator_mul_eq_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (J : Finset ι) {j j' : ℕ} (h : j ≠ j') : countEqIndicator α J j * countEqIndicator α J j' = 0

Distinct count indicators are incompatible.

theorem HavingProbability.funcProb_count_filter {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (J : Finset ι) (g : ℕ → Prop) [DecidablePred g] : (P.funcProb fun (v : X → Bool) => decide (g {i ∈ J | α i v = true}.card)) = ∑ j ∈ Finset.range (J.card + 1) with g j, P.funcProb (countEqIndicator α J j)

CDF assembly. For any predicate g on counts, the probability that the number of present contributors satisfies g is the sum of the point masses ρ_J(j) over the satisfying counts j ∈ {0, …, |J|}. For the six comparison operators the satisfying set is an interval.

theorem HavingProbability.countMass_zero {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (S : ι → Finset X) (hdep : ∀ (i : ι), (α i).DependsOn (S i)) (hdisj : Set.univ.Pairwise fun (i j : ι) => Disjoint (S i) (S j)) (J : Finset ι) : P.funcProb (countEqIndicator α J 0) = ∏ i ∈ J, (1 - P.funcProb (α i))

Empty-world mass. The probability that no contributor of J is present is ∏_{i ∈ J} (1 - p i).

theorem HavingProbability.count_ge_eq_absent_le {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (α : ι → BoolFunc X) (J : Finset ι) {C : ℕ} (hC : C ≤ J.card) : (fun (v : X → Bool) => decide (C ≤ {i ∈ J | α i v = true}.card)) = fun (v : X → Bool) => decide ({i ∈ J | (1 - α i) v = true}.card ≤ J.card - C)

Shorter-tail identity, event form. Counting the present contributors down from C is counting the absent contributors up to |J| - C: the two indicator functions coincide.

theorem HavingProbability.funcProb_count_ge_eq_absent_le {X : Type} [Fintype X] [DecidableEq X] {ι : Type} [Fintype ι] [DecidableEq ι] (P : ProbAssignment X) (α : ι → BoolFunc X) (J : Finset ι) {C : ℕ} (hC : C ≤ J.card) : (P.funcProb fun (v : X → Bool) => decide (C ≤ {i ∈ J | α i v = true}.card)) = P.funcProb fun (v : X → Bool) => decide ({i ∈ J | (1 - α i) v = true}.card ≤ J.card - C)

Shorter-tail identity, probability form: Pr[B ≥ C] = Pr[B' ≤ N − C] where B counts the present contributors and B' the absent ones. The right-hand side assembles from the point masses of the complemented contributors (1 - α i, marginals 1 - p i), which is the shorter summation when C exceeds N/2.

The possible-world HAVING provenance under a valuation

The predicate provenance of an aggregate comparison (Having.havingProv, over 𝔹[X]) is a ⊕-sum of one disjunct per non-empty possible world. Under a fixed valuation of the Boolean variables, exactly one disjunct survives: the one of the realized world, formed of the occurrences whose annotation is true. Consequently the predicate provenance evaluates to true exactly when the realized world is non-empty and satisfies the comparison – the bridge between the intensional possible-world semantics and probabilistic query evaluation: the probability of the predicate provenance is the probability that the realized world is non-empty and satisfies the comparison.

The section culminates in booleanHaving_pqe: for a Boolean query made of a Boolean combination of aggregate comparisons (HavingPred) applied on top of a non-aggregation query over a tuple-independent probabilistic database, the probability that a random world satisfies the query (booleanHavingProb, via the plain semantics HavingPred.modelsBoolean) equals the probability of its Boolean provenance (HavingPred.booleanProv). The non-aggregation operators are handled by randomWorld_evaluateAnnotated and the comparisons by the exactly-one-disjunct bridge, composed through the sorted-sublist identity groupSeq_randomWorld between the plain group sequence of a random world and the realized subsequence of the annotated group sequence.

def HavingProbability.realizedWorld {X T : Type} {m : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (v : X → Bool) : Finset (Fin U.length)

The world realized by a valuation v: the positions of the group sequence whose annotation evaluates to true under v.

Equations

• HavingProbability.realizedWorld U v = {i : Fin U.length | (U.get i).2 v = true}

theorem HavingProbability.worldAnn_eval_iff {X : Type} [Fintype X] [DecidableEq X] {N : ℕ} (α : Fin N → BoolFunc X) (W : Finset (Fin N)) (v : X → Bool) : Having.worldAnn α W v = true ↔ W = {i : Fin N | α i v = true}

Exactly one world annotation survives: under a valuation v, the factored world annotation of W is true iff W is the realized world.

theorem HavingProbability.chi_eval_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] (op : CompOp) (a c : T) (v : X → Bool) : Having.chi op a c v = true ↔ op.eval a c

Evaluation of the comparison characteristic χ_op.

theorem HavingProbability.havingProv_eval_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (t : Term T m) (f : SeqAggFunc T) (op : CompOp) (c : T) (v : X → Bool) : Having.havingProv U t f op c v = true ↔ (realizedWorld U v).Nonempty ∧ op.eval (Having.aggValOn U t f (realizedWorld U v)) c

PQE bridge for aggregate comparisons. Under a valuation v, the predicate provenance of f(t) op c on the group sequence U evaluates to true iff the realized world is non-empty and its aggregate value satisfies the comparison. Composed with the probability semantics, the probability of the predicate provenance is the probability, over random worlds, that a non-empty realized group satisfies the HAVING comparison.

theorem HavingProbability.multiset_sum_eval_eq_true_iff {X : Type} [Fintype X] [DecidableEq X] (s : Multiset (BoolFunc X)) (v : X → Bool) : s.sum v = true ↔ ∃ f ∈ s, f v = true

Pointwise evaluation of a Multiset.sum of BoolFuncs: the sum (OR) evaluates to true iff some summand does.

theorem HavingProbability.seqOf_filter_positions {β : Type} (P : β → Bool) (U : List β) : Having.seqOf U {i : Fin U.length | P (U.get i) = true} = List.filter P U

Selecting the positions whose element satisfies a Boolean predicate yields the filtered list.

theorem HavingProbability.seqOf_realizedWorld {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (v : X → Bool) : Having.seqOf U (realizedWorld U v) = List.filter (fun (p : AnnotatedTuple T (BoolFunc X) m) => p.2 v) U

The subsequence selected by the realized world is the sublist of occurrences whose annotation is true under the valuation.

theorem HavingProbability.realizedWorld_nonempty_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (v : X → Bool) : (realizedWorld U v).Nonempty ↔ ∃ p ∈ U, p.2 v = true

The realized world of a group is non-empty iff some occurrence of the group survives the valuation.

theorem HavingProbability.groupSeq_randomWorld {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m n₁ : ℕ} [HasAltLinearOrder (BoolFunc X)] (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T (BoolFunc X) m) (g : Tuple T n₁) (v : X → Bool) : Relation.groupSeq is (randomWorld v r) g = List.map Prod.fst (Having.seqOf (Having.havingGroup is r g) (realizedWorld (Having.havingGroup is r g) v))

The plain group sequence of a random world is the realized subsequence of the annotated group sequence: both are lists of the same multiset (the realized occurrences of the group), sorted along ≼.

theorem HavingProbability.randomWorld_key_mem_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m n₁ : ℕ} [HasAltLinearOrder (BoolFunc X)] (is : Tuple (Fin m) n₁) (r : AnnotatedRelation T (BoolFunc X) m) (g : Tuple T n₁) (v : X → Bool) : g ∈ Multiset.map (fun (u : Tuple T m) (k : Fin n₁) => u (is k)) (randomWorld v r) ↔ (realizedWorld (Having.havingGroup is r g) v).Nonempty

A key is realized in the random world iff the realized world of its group sequence is non-empty.

theorem HavingProbability.HavingPred.provAux_eval_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m n₁ : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (g : Tuple T n₁) (v : X → Bool) (negated : Bool) (ψ : HavingPred T m n₁) : HavingPred.provAux U g negated ψ v = true ↔ (realizedWorld U v).Nonempty ∧ if negated = true then ¬HavingPred.holdsOnSeq (List.map Prod.fst (Having.seqOf U (realizedWorld U v))) g ψ else HavingPred.holdsOnSeq (List.map Prod.fst (Having.seqOf U (realizedWorld U v))) g ψ

PQE bridge for Boolean combinations, with polarity. Under a valuation, the polarity-aware predicate provenance of ψ is true iff the realized world of the group is non-empty and ψ (negated according to the polarity) holds classically on the realized occurrence sequence.

theorem HavingProbability.HavingPred.prov_eval_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] {m n₁ : ℕ} (U : List (AnnotatedTuple T (BoolFunc X) m)) (g : Tuple T n₁) (v : X → Bool) (ψ : HavingPred T m n₁) : HavingPred.prov U g ψ v = true ↔ (realizedWorld U v).Nonempty ∧ HavingPred.holdsOnSeq (List.map Prod.fst (Having.seqOf U (realizedWorld U v))) g ψ

PQE bridge for Boolean combinations of aggregate comparisons. Under a valuation, the predicate provenance of ψ on the group sequence U is true iff the realized world is non-empty and ψ holds classically on the realized occurrence sequence.

theorem HavingProbability.HavingPred.booleanProv_eval_iff {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T] [HasAltLinearOrder (BoolFunc X)] {m n₁ : ℕ} (q : Query T m) (hq : q.source) (Î : AnnotatedDatabase T (BoolFunc X)) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) (v : X → Bool) : HavingPred.booleanProv q hq Î is ψ v = true ↔ HavingPred.modelsBoolean (AnnotatedDatabase.randomWorld v Î) q is ψ

Characteristic property of the Boolean provenance. Under a valuation, the Boolean provenance of a Boolean HAVING query is true iff the query holds on the corresponding possible world.

noncomputable def HavingProbability.booleanHavingProb {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) {T : Type} [ValueType T] {m n₁ : ℕ} (q : Query T m) (Î : AnnotatedDatabase T (BoolFunc X)) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) : ℚ

Probability that a random world of Î satisfies a Boolean HAVING query: the sum of Pr(v) over the valuations whose possible world does.

Equations

• HavingProbability.booleanHavingProb P q Î is ψ = ∑ v : X → Bool, if HavingPred.modelsBoolean (AnnotatedDatabase.randomWorld v Î) q is ψ then P.valProb v else 0

theorem HavingProbability.booleanHaving_pqe {X : Type} [Fintype X] [DecidableEq X] (P : ProbAssignment X) {T : Type} [ValueType T] [HasAltLinearOrder (BoolFunc X)] {m n₁ : ℕ} (q : Query T m) (hq : q.source) (Î : AnnotatedDatabase T (BoolFunc X)) (is : Tuple (Fin m) n₁) (ψ : HavingPred T m n₁) : booleanHavingProb P q Î is ψ = P.funcProb (HavingPred.booleanProv q hq Î is ψ)

Probabilistic query evaluation through the HAVING provenance. For a Boolean query made of a Boolean combination ψ of aggregate comparisons applied on top of a non-aggregation query q grouped by is, over a tuple-independent probabilistic database, the probability that a random world satisfies the query equals the probability of its Boolean provenance (the ⊕-sum, over the group keys, of the predicate provenance of ψ). The non-aggregation operators of q are handled by the correctness of intensional probabilistic query evaluation (ProbAssignment.theorem_12 machinery via randomWorld_evaluateAnnotated), and the aggregate comparison by the exactly-one-disjunct bridge HavingPred.prov_eval_iff.

Home · Documentation · Publications · Contributors · Source · Cite