Statistical distance of independent products

Replacing independent coordinates costs at most the sum of their individual distances. The same bound holds when the coordinates are conditionally independent given a shared public sample: the sample is drawn once and remains visible on both sides. For k independent draws from one law, replacing the law costs at most k times its distance; this is the statistical hop that replaces approximately sampled values by exactly sampled ones.

Main results

• Cslib.Probability.PMF.dist_pi_le_sum: distance between products is at most the sum of distances.
• Cslib.Probability.PMF.dist_bind_pair_pi_le_sum: retain the shared public sample in that bound.
• Cslib.Probability.PMF.dist_iid_le: k independent draws are at distance at most k times the distance of one draw.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 3.11.

theorem Cslib.Probability.PMF.dist_pi_update_le {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] [DecidableEq ι] (p : (i : ι) → PMF (α i)) (i : ι) (a b : PMF (α i)) : dist (pi (Function.update p i a)) (pi (Function.update p i b)) ≤ dist a b

Replacing one independent coordinate cannot cost more than its own statistical distance.

theorem Cslib.Probability.PMF.dist_pi_le_sum {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] [DecidableEq ι] (p q : (i : ι) → PMF (α i)) : dist (pi p) (pi q) ≤ ∑ i : ι, dist (p i) (q i)

The statistical distance of finite independent products is at most the sum of distances.

theorem Cslib.Probability.PMF.dist_bind_pair_pi_le_sum {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] [DecidableEq ι] {Seed : Type u_3} [Fintype Seed] (seed : PMF Seed) (p q : Seed → (i : ι) → PMF (α i)) : dist (seed.bind fun (s : Seed) => PMF.map (fun (x : (i : ι) → α i) => (s, x)) (pi (p s))) (seed.bind fun (s : Seed) => PMF.map (fun (x : (i : ι) → α i) => (s, x)) (pi (q s))) ≤ ∑ i : ι, dist (seed.bind fun (s : Seed) => PMF.map (fun (x : α i) => (s, x)) (p s i)) (seed.bind fun (s : Seed) => PMF.map (fun (x : α i) => (s, x)) (q s i))

A common public sample may be retained when replacing conditionally independent coordinates. There is no requirement that the coordinates be independent after the public sample is hidden.

theorem Cslib.Probability.PMF.dist_iid_le {β : Type u_3} [Fintype β] (μ ν : PMF β) (k : ℕ) : dist (iid μ k) (iid ν k) ≤ ↑k * dist μ ν

Independent draws. k independent draws from μ and from ν are at statistical distance at most k times the distance between μ and ν.