Probability identities for seed-indexed output families

The retained-seed weighting is a deterministic image of a source and seed pair. Its finite tests agree with weighted seeded tests, including repeated output values. Normalized conditional distributions give a normalized joint distribution whenever the seed type is nonempty.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedSeededOutput_eq_mapWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (C : α → Seed → Ω) : weightedSeededOutput p C = mapWeight (fun (xy : α × Seed) => (xy.2, C xy.1 xy.2)) fun (xy : α × Seed) => p xy.1 / ↑(Fintype.card Seed)

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] [Nonempty Seed] (q : Seed → Ω → ℝ) (probability : ∀ (y : Seed), IsProbabilityWeight (q y)) : IsProbabilityWeight (seedFamilyWeight q)

theorem Algebraic.Cutwidth.Extractor.Internal.probabilityWeight_weightedSeededOutput {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] {p : α → ℝ} (probability : IsProbabilityWeight p) (C : α → Seed → Ω) : IsProbabilityWeight (weightedSeededOutput p C)

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_weightedSeededOutput {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (C : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightTestProb (weightedSeededOutput p C) T = weightedSeededTestProb p C T

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] (q : Seed → Ω → ℝ) (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight q) T = (∑ yz ∈ T, q yz.1 yz.2) / ↑(Fintype.card Seed)

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_seedFamilyWeight_uniform {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight fun (x : Seed) => uniformWeight Ω) T = uniformSeededTestProb T

theorem Algebraic.Cutwidth.Extractor.Internal.weightTestProb_seedFamilyWeight_mixture {ι : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype ι] [Fintype Seed] (w : ι → ℝ) (q : ι → Seed → Ω → ℝ) (T : Finset (Seed × Ω)) : weightTestProb (seedFamilyWeight fun (y : Seed) (z : Ω) => ∑ i : ι, w i * q i y z) T = ∑ i : ι, w i * weightTestProb (seedFamilyWeight (q i)) T

theorem Algebraic.Cutwidth.Extractor.Internal.cappedWeight_map_injective {α : Type u_1} {β : Type u_2} [Fintype α] {p : α → ℝ} {K : ℕ} (cap : CappedWeight p K) (f : α → β) (injective : Function.Injective f) : CappedWeight (mapWeight f p) K