Finite seeded neighbors and test probabilities #
The neighbor set retains the seed coordinate. Test probabilities count all source and seed pairs, including pairs with the same output, before dividing by the number of pairs. These definitions describe uniform finite sources; they do not assert anything about arbitrary probability weights.
noncomputable def
Algebraic.Cutwidth.Extractor.seededNeighborSet
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
(C : α → Seed → Ω)
(P : Finset α)
:
All seed and output pairs reached from the finite source support.
Equations
- Algebraic.Cutwidth.Extractor.seededNeighborSet C P = P.biUnion fun (x : α) => Finset.image (fun (y : Seed) => (y, C x y)) Finset.univ
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.seededTestProb
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
(C : α → Seed → Ω)
(T : Finset (Seed × Ω))
:
The probability that a uniform independent source and seed pass a test. The value is zero when either sampling type is empty.
Equations
- Algebraic.Cutwidth.Extractor.seededTestProb C T = ↑{xy : α × Seed | (xy.2, C xy.1 xy.2) ∈ T}.card / (↑(Fintype.card α) * ↑(Fintype.card Seed))