Tests of supplied finite mixtures of seeded sources #
Each component samples its own finite source type uniformly and uses an
independent uniform seed. The mixture weights choose the component before
sampling either value. Normalization and nonnegativity are hypotheses of
the probability theorems, rather than requirements of the finite sum.
Empty sampling types use the zero convention of seededTestProb.
noncomputable def
Algebraic.Cutwidth.Extractor.seededMixtureTestProb
{ι : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype ι]
[Fintype Seed]
{Source : ι → Type u_4}
[(i : ι) → Fintype (Source i)]
(w : ι → ℝ)
(C : (i : ι) → Source i → Seed → Ω)
(T : Finset (Seed × Ω))
:
Test probability for a supplied mixture when its weights are nonnegative and sum to one. Component source types may differ; the seed type is shared.
Equations
- Algebraic.Cutwidth.Extractor.seededMixtureTestProb w C T = ∑ i : ι, w i * Algebraic.Cutwidth.Extractor.seededTestProb (C i) T