Probability identities for HAVING aggregate comparisons under independence

This file formalises 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 factorisation (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).

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 factorisation

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 factorisation 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 factorisation

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 factorisation 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).

Home · Documentation · Publications · Contributors · Source · Cite