Finite mixture identities for retained tags

Deterministic pushforwards are linear in arbitrary real weights. Retaining a mixture tag makes total variation an exact weighted sum; forgetting it can only decrease the distance. Uniform seed families are a specialization, including the empty seed type under the usual zero-division convention.

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_mul {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (c : ℝ) (p : α → ℝ) : (mapWeight f fun (x : α) => c * p x) = fun (y : β) => c * mapWeight f p y

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [Fintype α] (f : α → β) (p : ι → α → ℝ) : (mapWeight f fun (x : α) => ∑ i : ι, p i x) = fun (y : β) => ∑ i : ι, mapWeight f (p i) y

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_mixture {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [Fintype α] (f : α → β) (w : ι → ℝ) (p : ι → α → ℝ) : (mapWeight f fun (x : α) => ∑ i : ι, w i * p i x) = fun (y : β) => ∑ i : ι, w i * mapWeight f (p i) y

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_tagged {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [Fintype α] (f : ι → α → β) (w : ι → ℝ) (p : ι → α → ℝ) : (mapWeight (fun (ix : ι × α) => (ix.1, f ix.1 ix.2)) fun (ix : ι × α) => w ix.1 * p ix.1 ix.2) = fun (iz : ι × β) => w iz.1 * mapWeight (f iz.1) (p iz.1) iz.2

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_seedFamilyWeight {Seed : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype Seed] [Fintype α] (f : Seed → α → β) (p : Seed → α → ℝ) : mapWeight (fun (yz : Seed × α) => (yz.1, f yz.1 yz.2)) (seedFamilyWeight p) = seedFamilyWeight fun (y : Seed) => mapWeight (f y) (p y)

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

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_tagged_mixture {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] (w : ι → ℝ) (p q : ι → α → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ w i) : (weightDist (fun (ix : ι × α) => w ix.1 * p ix.1 ix.2) fun (ix : ι × α) => w ix.1 * q ix.1 ix.2) = ∑ i : ι, w i * weightDist (p i) (q i)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_mixture_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] (w : ι → ℝ) (p q : ι → α → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ w i) : (weightDist (fun (x : α) => ∑ i : ι, w i * p i x) fun (x : α) => ∑ i : ι, w i * q i x) ≤ ∑ i : ι, w i * weightDist (p i) (q i)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (p q : Seed → Ω → ℝ) : weightDist (seedFamilyWeight p) (seedFamilyWeight q) = (∑ y : Seed, weightDist (p y) (q y)) / ↑(Fintype.card Seed)

theorem Algebraic.Cutwidth.Extractor.Internal.weightDist_weightedSeededOutput_seedFamilyWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (p : α → ℝ) (C : α → Seed → Ω) (q : Seed → Ω → ℝ) : weightDist (weightedSeededOutput p C) (seedFamilyWeight q) = (∑ y : Seed, weightDist (mapWeight (fun (x : α) => C x y) p) (q y)) / ↑(Fintype.card Seed)