Uniform subset estimates

This file contains estimates for the total variation distance between the uniform distribution on a finite type and the uniform distribution on a nonempty finite subset, together with averaging bounds for [0,1]-valued functions. The uniform-subset total-variation identity is proved by transport through Mathlib probability mass functions.

theorem MIPStarRE.LDT.totalVariationDistance_uniformDistribution_uniformOnFinset_eq {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (s : Finset α) (hs : s.Nonempty) : totalVariationDistance (uniformDistribution α) (Distribution.uniformOnFinset s) = 1 - ↑s.card / ↑(Fintype.card α)

Total variation between the uniform distribution on a finite ambient type and the uniform distribution on a nonempty finite subset.

This is the elementary finite identity TV(uniform α, uniform s) = 1 - |s| / |α|. The proof transports the project Distribution statement to Mathlib's uniform probability mass functions.

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_le_uniformDistribution_add_totalVariationDistance {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (s : Finset α) (hs : s.Nonempty) (f : α → Error) (hf_nonneg : ∀ (a : α), 0 ≤ f a) (hf_le_one : ∀ (a : α), f a ≤ 1) : avgOver (Distribution.uniformOnFinset s) f ≤ avgOver (uniformDistribution α) f + totalVariationDistance (uniformDistribution α) (Distribution.uniformOnFinset s)

A [0,1]-valued function averaged over a nonempty finite subset is bounded by its ambient uniform average plus the total variation distance between the two uniform distributions.