Documentation

Complexity.Probability.StatisticalDistance

Statistical distance with public side information #

Revealing a shared sample makes the joint distance exactly the average conditional distance. Its square is bounded by the corresponding average squared distance. Statistical distance is the probability gap on the event where one distribution exceeds the other, and half of Mathlib's total variation distance tvDist of the induced measures. These statements reuse the upstream finite-PMF metric and its enumeration instances.

Main results #

References #

Adapted from Probability/StatisticalDistance.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The metric itself remains the upstream one.

source
theorem Cslib.Probability.PMF.dist_filter {α : Type u_1} [Fintype α] (p : PMF α) (event : Set α) (hevent : ∃ a ∈ event, a ∈ p.support) :
dist p (p.filter event hevent) = (p.toOuterMeasure eventᶜ).toReal

Conditioning on a possible event changes the distribution by exactly the probability discarded outside that event.

source
theorem Cslib.Probability.PMF.dist_bind_pair {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : PMF α) (f g : α → PMF β) :
dist (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (f a)) (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (g a)) = ∑ a : α, (p a).toReal * dist (f a) (g a)

With a shared revealed input, distance is the average distance of the conditional outputs.

source
theorem Cslib.Probability.PMF.dist_bind_pair_sq_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : PMF α) (f g : α → PMF β) :
dist (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (f a)) (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (g a)) ^ 2 ≤ ∑ a : α, (p a).toReal * dist (f a) (g a) ^ 2

Squared distance with a shared revealed input is at most the average squared distance.

source
theorem Cslib.Probability.PMF.abs_sum_mul_sub_le {α : Type u_1} [Fintype α] (p q : PMF α) (score : α → ℝ) {bound : ℝ} (hscore : ∀ (a : α), |score a| ≤ bound) :
|∑ a : α, (p a).toReal * score a - ∑ a : α, (q a).toReal * score a| ≤ 2 * bound * dist p q

Changing the distribution changes a bounded real-valued score by at most twice its absolute bound times statistical distance. Signed prediction scores may use bound = 1.

source
theorem Cslib.Probability.PMF.dist_bind_left_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : PMF α) (f : α → PMF β) (q : PMF β) :
dist (p.bind f) q ≤ ∑ a : α, (p a).toReal * dist (f a) q

Convexity of statistical distance in the first argument: the distance of a mixture p.bind f from q is at most the p-weighted average distance of f a from q.

source
theorem Cslib.Probability.PMF.dist_bind_left_le_of_le {α : Type u_1} {β : Type u_2} [Finite α] [Fintype β] (p : PMF α) (f : α → PMF β) (q : PMF β) {δ : ℝ} (h : ∀ a ∈ p.support, dist (f a) q ≤ δ) :
dist (p.bind f) q ≤ δ

If every component f a in the support of p is within δ of q, so is p.bind f.

source
theorem Cslib.Probability.PMF.dist_uniformOfFintype_bool (p : PMF Bool) :
dist p (uniformOfFintype Bool) = |(p true).toReal - 1 / 2|

Statistical distance on Bool from the uniform distribution is the bias |p(true) - 1 / 2|.

source
theorem Cslib.Probability.PMF.dist_eq_sum_filter_lt {α : Type u_1} [Fintype α] (p q : PMF α) :
dist p q = ∑ a : α with (q a).toReal < (p a).toReal, ((p a).toReal - (q a).toReal)

Statistical distance is the probability gap on the event where p exceeds q.

source
theorem Cslib.Probability.PMF.dist_eq_tvDist_toMeasure_div_two {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p q : PMF α) :
dist p q = MeasureTheory.tvDist p.toMeasure q.toMeasure / 2

Statistical distance is half of Mathlib's total variation distance tvDist of the PMF measures.