Product-seed averaging and deterministic composition

Reassociating uniform seeds gives the product seed denominator. Finite distance averaging then shows that adding a fresh independent seed and applying a deterministic map cannot increase an earlier joint error. The same finite pushforward identities identify successive seeded programs with their deterministic composition.

theorem Algebraic.Cutwidth.Extractor.Internal.seedFamilyWeight_product {Earlier : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Earlier] [Fintype Fresh] [Fintype Ω] (p : Earlier → Fresh → Ω → ℝ) : mapWeight (⇑(Equiv.prodAssoc Earlier Fresh Ω).symm) (seedFamilyWeight fun (s : Earlier) => seedFamilyWeight (p s)) = seedFamilyWeight fun (sy : Earlier × Fresh) => p sy.1 sy.2

theorem Algebraic.Cutwidth.Extractor.Internal.retainedSeedStep_seedFamilyWeight {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p : Earlier → X → ℝ) : retainedSeedStep F (seedFamilyWeight p) = seedFamilyWeight fun (sy : Earlier × Fresh) => mapWeight (fun (x : X) => F sy.1 x sy.2) (p sy.1)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_seedFamilyWeight_product {Earlier : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Earlier] [Fintype Fresh] [Fintype Ω] (p q : Earlier → Fresh → Ω → ℝ) : weightDist (seedFamilyWeight fun (sy : Earlier × Fresh) => p sy.1 sy.2) (seedFamilyWeight fun (sy : Earlier × Fresh) => q sy.1 sy.2) = (∑ s : Earlier, weightDist (seedFamilyWeight (p s)) (seedFamilyWeight (q s))) / ↑(Fintype.card Earlier)

theorem Algebraic.Cutwidth.Extractor.Internal.weightedSeededOutput_dist_le {X : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype X] [Fintype Fresh] [Fintype Ω] (p q : X → ℝ) (F : X → Fresh → Ω) : weightDist (weightedSeededOutput p F) (weightedSeededOutput q F) ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.retainedSeedStep_dist_le {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p q : Earlier × X → ℝ) : weightDist (retainedSeedStep F p) (retainedSeedStep F q) ≤ weightDist p q

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_retainedSeedStep {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] [Nonempty Fresh] {p : Earlier × X → ℝ} (probability : IsProbabilityWeight p) (F : Earlier → X → Fresh → Ω) : IsProbabilityWeight (retainedSeedStep F p)

theorem Algebraic.Cutwidth.Extractor.Internal.retainedSeedStep_weightedSeededOutput {A : Type u_1} {Earlier : Type u_2} {Fresh : Type u_3} {X : Type u_4} {Ω : Type u_5} [Fintype A] [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p : A → ℝ) (E : A → Earlier → X) : retainedSeedStep F (weightedSeededOutput p E) = weightedSeededOutput p fun (a : A) (sy : Earlier × Fresh) => F sy.1 (E a sy.1) sy.2