Product of Experts

Multiplicative combination of probability distributions.

def Core.ProductOfExperts.productOfExperts {α : Type} (ps : List (α → ℚ)) (support : List α) : α → ℚ

Product of Experts: combine distributions multiplicatively.

Equations

• One or more equations did not get rendered due to their size.

def Core.ProductOfExperts.poe2 {α : Type} (p₁ p₂ : α → ℚ) (support : List α) : α → ℚ

Product of two experts.

Equations

• Core.ProductOfExperts.poe2 p₁ p₂ support = Core.ProductOfExperts.productOfExperts [p₁, p₂] support

def Core.ProductOfExperts.poe3 {α : Type} (p₁ p₂ p₃ : α → ℚ) (support : List α) : α → ℚ

Product of three experts.

Equations

• Core.ProductOfExperts.poe3 p₁ p₂ p₃ support = Core.ProductOfExperts.productOfExperts [p₁, p₂, p₃] support

def Core.ProductOfExperts.unnormalizedProduct {α : Type} (ps : List (α → ℚ)) : α → ℚ

Unnormalized product: multiply expert scores without normalizing.

Equations

• Core.ProductOfExperts.unnormalizedProduct ps a = List.foldl (fun (acc : ℚ) (p : α → ℚ) => acc * p a) 1 ps

def Core.ProductOfExperts.normalizeOver {α : Type} (f : α → ℚ) (support : List α) : α → ℚ

Normalize a scoring function over a finite support.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.ProductOfExperts.poe_eq_unnorm_then_norm {α : Type} (ps : List (α → ℚ)) (support : List α) : productOfExperts ps support = normalizeOver (unnormalizedProduct ps) support

PoE equals unnormalized product followed by normalization.

theorem Core.ProductOfExperts.foldl_mul_zero_init {α : Type} (ps : List (α → ℚ)) (a : α) : List.foldl (fun (acc : ℚ) (p : α → ℚ) => acc * p a) 0 ps = 0

Folding multiplication with zero accumulator stays zero.

theorem Core.ProductOfExperts.foldl_mul_zero {α : Type} (ps : List (α → ℚ)) (a : α) (init : ℚ) (hp : ∃ p ∈ ps, p a = 0) : List.foldl (fun (acc : ℚ) (p : α → ℚ) => acc * p a) init ps = 0

Folding multiplication absorbs zero.

theorem Core.ProductOfExperts.poe_single {α : Type} (p : α → ℚ) (support : List α) : productOfExperts [p] support = normalizeOver p support

PoE with single expert returns normalized version of that expert.

theorem Core.ProductOfExperts.poe_zero_absorbing {α : Type} (ps : List (α → ℚ)) (support : List α) (a : α) (hp : ∃ p ∈ ps, p a = 0) : productOfExperts ps support a = 0 ∨ ∃ a' ∈ support, productOfExperts ps support a' > 0

PoE is zero-absorbing: if any expert gives zero, product is zero.

theorem Core.ProductOfExperts.foldl_add_one {α : Type} (xs : List α) (init : ℚ) : List.foldl (fun (acc : ℚ) (x : α) => acc + 1) init xs = init + ↑xs.length

Foldl adding 1 with any init.

theorem Core.ProductOfExperts.foldl_add_one_eq_length {α : Type} (xs : List α) : List.foldl (fun (acc : ℚ) (x : α) => acc + 1) 0 xs = ↑xs.length

Foldl adding 1 equals length.

theorem Core.ProductOfExperts.poe_empty {α : Type} (support : List α) (a : α) : productOfExperts [] support a = if support.length = 0 then 0 else 1 / ↑support.length

PoE with empty expert list gives uniform.

def Core.ProductOfExperts.linearCombine (lam v₁ v₂ : ℚ) : ℚ

Linear combination of two values.

Equations

• Core.ProductOfExperts.linearCombine lam v₁ v₂ = (1 - lam) * v₁ + lam * v₂

theorem Core.ProductOfExperts.linear_not_zero_absorbing : linearCombine (1 / 2) 0 1 ≠ 0

Linear combination is NOT zero-absorbing.

theorem Core.ProductOfExperts.poe2_zero_absorbing {α : Type} (p₁ p₂ : α → ℚ) (support : List α) (a : α) : p₁ a = 0 → poe2 p₁ p₂ support a = 0 ∨ List.foldl (fun (acc : ℚ) (x : α) => acc + p₁ x * p₂ x) 0 support = 0

PoE IS zero-absorbing (for the 2-expert case).

def Core.ProductOfExperts.listArgmax {α : Type} (xs : List α) (f : α → ℚ) : Option α

Find the element with maximum value according to a scoring function.

Equations

• One or more equations did not get rendered due to their size.

structure Core.ProductOfExperts.FactoredDist (α : Type) : Type

A factored distribution in SDS style.

• selectionalExpert : α → ℚ
• scenarioExpert : α → ℚ
• support : List α

def Core.ProductOfExperts.FactoredDist.combine {α : Type} (d : FactoredDist α) : α → ℚ

Combine a factored distribution using PoE.

Equations

• d.combine = Core.ProductOfExperts.poe2 d.selectionalExpert d.scenarioExpert d.support

def Core.ProductOfExperts.FactoredDist.unnormScores {α : Type} (d : FactoredDist α) : α → ℚ

Get the unnormalized scores.

Equations

• d.unnormScores a = d.selectionalExpert a * d.scenarioExpert a

def Core.ProductOfExperts.FactoredDist.hasConflict {α : Type} [BEq α] (d : FactoredDist α) : Bool

Detect conflict: experts disagree on the mode.

Equations

• One or more equations did not get rendered due to their size.

def Core.ProductOfExperts.FactoredDist.conflictDegree {α : Type} [BEq α] (d : FactoredDist α) : ℚ

Get the degree of conflict between expert modes.

Equations

• One or more equations did not get rendered due to their size.

def Core.ProductOfExperts.weightedPoe {α : Type} (experts : List ((α → ℚ) × ℚ)) (support : List α) : α → ℚ

Weighted PoE: P(x) ∝ Π_i p_i(x)^{β_i}.

Equations

• One or more equations did not get rendered due to their size.

def Core.ProductOfExperts.bayesianPoe {α : Type} (likelihood prior : α → ℚ) (support : List α) : α → ℚ

Bayesian update as PoE: posterior ∝ likelihood × prior.

Equations

• Core.ProductOfExperts.bayesianPoe likelihood prior support = Core.ProductOfExperts.poe2 likelihood prior support

theorem Core.ProductOfExperts.unnormalizedProduct_comm {α : Type} (p q : α → ℚ) (a : α) : unnormalizedProduct [p, q] a = unnormalizedProduct [q, p] a

Unnormalized PoE is order-independent.

theorem Core.ProductOfExperts.poe_comm {α : Type} (p q : α → ℚ) (support : List α) : productOfExperts [p, q] support = productOfExperts [q, p] support

PoE with reordered experts gives same result.