Marginal probability masses on coordinate patterns

The marginal of a finite real-valued probability mass function is the sum of its masses over all completions of a selected-coordinate pattern. This differs from coordinateMarginal, which averages normalized densities.

noncomputable def Complexity.BooleanAnalysis.coordinateMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (selected : ι → Bool) (pattern : { i : ι // selected i = true } → Bool) : ℝ

Sum of the masses of all completions of a coordinate pattern. For a nonnegative mass function summing to one, this is the probability of the pattern.

Equations

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