Statistical distance under finite mixtures

Retaining a finite mixture tag gives exact averaging of component total variation distances. Forgetting the tag gives the corresponding upper bound. Uniform retained-seed families therefore have distance equal to the average of their conditional distances, including empty seed types.

The component weights need not be probability distributions. Only the mixture coefficients in the distance identities must be nonnegative; the pushforward and seed-family linearity identities hold for all real coefficients. These are finite algebraic identities, with no claim about computing arbitrary real weights.

theorem Algebraic.Cutwidth.Extractor.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

A deterministic pushforward commutes with arbitrary scalar multiplication.

theorem Algebraic.Cutwidth.Extractor.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

A deterministic pushforward commutes with finite sums of arbitrary weights.

theorem Algebraic.Cutwidth.Extractor.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

Finite mixtures commute with deterministic maps, without sign or mass assumptions.

theorem Algebraic.Cutwidth.Extractor.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

A map that keeps the mixture tag pushes each component forward separately.

theorem Algebraic.Cutwidth.Extractor.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)

Keeping the seed commutes with pushing forward its conditional output family.

theorem Algebraic.Cutwidth.Extractor.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

Retained-seed weights are linear in arbitrary finite mixtures of conditional laws.

theorem Algebraic.Cutwidth.Extractor.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)

Retaining the tag makes mixture distance exactly the weighted sum of component distances.

theorem Algebraic.Cutwidth.Extractor.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)

Forgetting mixture tags can only reduce the weighted sum of component distances.

theorem Algebraic.Cutwidth.Extractor.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)

Retained-seed distance is the average conditional distance, also for an empty seed type.

theorem Algebraic.Cutwidth.Extractor.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)

An actual retained-seed output is compared with its witness by averaging fiber distances.