Finite test identities for composition with an independent seed

These identities keep both seeds and count every source occurrence. A fresh seed averages pullback tests of the first map; conditioning on the first seed averages tests of the second map. Embeddings transfer uniform sources to uniform image supports without discarding multiplicity in the original map.

noncomputable def Algebraic.Cutwidth.Extractor.Internal.compositionPullback {Seed : Type u_1} {Fresh : Type u_2} {Z : Type u_3} {Ω : Type u_4} [Fintype Seed] [Fintype Z] (H : Z → Fresh → Ω) (T : Finset ((Seed × Fresh) × Ω)) (a : Fresh) : Finset (Seed × Z)

Pull back a composed joint test while fixing the fresh second seed.

Equations

• Algebraic.Cutwidth.Extractor.Internal.compositionPullback H T a = {yz : Seed × Z | ((yz.1, a), H yz.2 a) ∈ T}

noncomputable def Algebraic.Cutwidth.Extractor.Internal.compositionSlice {Seed : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Fresh] [Fintype Ω] (T : Finset ((Seed × Fresh) × Ω)) (y : Seed) : Finset (Fresh × Ω)

Slice a composed joint test at its first seed.

Equations

• Algebraic.Cutwidth.Extractor.Internal.compositionSlice T y = {az : Fresh × Ω | ((y, az.1), az.2) ∈ T}

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_eq_indicator_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (C : α → Seed → Ω) (T : Finset (Seed × Ω)) : seededTestProb C T = (∑ x : α, ∑ y : Seed, if (y, C x y) ∈ T then 1 else 0) / (↑(Fintype.card α) * ↑(Fintype.card Seed))

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_comp_pullback {α : Type u_1} {Seed : Type u_2} {Fresh : Type u_3} {Z : Type u_4} {Ω : Type u_5} [Fintype α] [Fintype Seed] [Fintype Fresh] [Fintype Z] (C : α → Seed → Z) (H : Z → Fresh → Ω) (T : Finset ((Seed × Fresh) × Ω)) : seededTestProb (fun (x : α) (ya : Seed × Fresh) => H (C x ya.1) ya.2) T = (∑ a : Fresh, seededTestProb C (compositionPullback H T a)) / ↑(Fintype.card Fresh)

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_comp_slice {α : Type u_1} {Seed : Type u_2} {Fresh : Type u_3} {Z : Type u_4} {Ω : Type u_5} [Fintype α] [Fintype Seed] [Fintype Fresh] [Fintype Ω] (g : Seed → α → Z) (H : Z → Fresh → Ω) (T : Finset ((Seed × Fresh) × Ω)) : seededTestProb (fun (x : α) (ya : Seed × Fresh) => H (g ya.1 x) ya.2) T = (∑ y : Seed, seededTestProb (fun (x : α) (a : Fresh) => H (g y x) a) (compositionSlice T y)) / ↑(Fintype.card Seed)

theorem Algebraic.Cutwidth.Extractor.Internal.uniformSeededTestProb_eq_indicator_sum {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : uniformSeededTestProb T = (∑ y : Seed, ∑ z : Ω, if (y, z) ∈ T then 1 else 0) / (↑(Fintype.card Seed) * ↑(Fintype.card Ω))

theorem Algebraic.Cutwidth.Extractor.Internal.uniformSeededTestProb_slice {Seed : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Fresh] [Fintype Ω] (T : Finset ((Seed × Fresh) × Ω)) : uniformSeededTestProb T = (∑ y : Seed, uniformSeededTestProb (compositionSlice T y)) / ↑(Fintype.card Seed)

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_embedding {α : Type u_1} {Seed : Type u_2} {Z : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype Seed] (g : α ↪ Z) (H : Z → Seed → Ω) (T : Finset (Seed × Ω)) : seededTestProb (fun (x : α) (a : Seed) => H (g x) a) T = seededTestProb (fun (z : ↥(Finset.map g Finset.univ)) => H ↑z) T