Conditioning a product distribution with side information

Raz's conditioning lemma (Cslib.Probability.PMF.sum_sq_dist_map_filter_pi_le) conditions a product distribution on an event about its coordinates. Holenstein applies it to events that also involve side information: a pair (u, v) drawn from a joint distribution whose first marginal is a product pi p, and an event W about the pair. The conditioned marginal of u still has divergence at most ln (1 / Pr[W]) from pi p, because its masses are at most those of pi p divided by Pr[W] (sum_mul_log_div_le_log_of_le), so the coordinates move by ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖² ≤ ln (1 / Pr[W]) / 2 (sum_sq_dist_map_filter_le) Holenstein, proof of Corollary 6.

Holenstein's Corollary 6 (sum_dist_filter_sideJoint_le) lets the coordinates be independent only given a further random variable t, and lets the side information v depend on t and u: with t ~ μ and (u, v) ~ J t, where the first marginal of J t is the product pi (K · t), ∑ⱼ ‖P_{TV Uⱼ | W} - P_{TV | W} P_{Uⱼ | T}‖ ≤ √(k · ln (|V| / Pr[W]) / 2). Each squared distance is bounded by the average squared conditional distance after revealing (t, v) (dist_bind_pair_sq_le). Given (t, v), the law of u is that of J t conditioned on the slice of W at (t, v) (conditionalSnd_filter_sideJoint), so the lemma above applies; the bound ln x ≤ x - 1 and Cauchy–Schwarz combine the slices. Holenstein uses the support V* of v under W where this statement uses the whole alphabet V, which can only make the bound here weaker; the factor 1 / 2 from Pinsker's inequality in nats makes it stronger, since ln x / 2 ≤ log₂ x for x ≥ 1.

Main definitions

• Cslib.Probability.PMF.sideJoint: the law of ((t, v), u).

Main results

• Cslib.Probability.PMF.sum_mul_log_div_le_log_of_le: divergence of a distribution dominated by a multiple of another.
• Cslib.Probability.PMF.sum_sq_dist_map_filter_le: Raz's conditioning lemma with side information.
• Cslib.Probability.PMF.dist_map_pair_bind_eq: distance after revealing a first component.
• Cslib.Probability.PMF.sum_dist_filter_sideJoint_le: Holenstein's Corollary 6.

References

• T. Holenstein, Parallel repetition: simplifications and the no-signaling case

theorem Cslib.Probability.PMF.sum_mul_log_div_le_log_of_le {α : Type u_1} [Fintype α] {p q : PMF α} {c : ℝ} (hc : 0 < c) (h : ∀ (a : α), (p a).toReal ≤ (q a).toReal / c) : ∑ a : α, (p a).toReal * Real.log ((p a).toReal / (q a).toReal) ≤ Real.log (1 / c)

If the masses of p are at most those of q divided by c > 0, the divergence of p from q is at most ln (1 / c).

theorem Cslib.Probability.PMF.sum_sq_dist_map_filter_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] {V : Type u_4} [Finite V] (p : (i : ι) → PMF (β i)) (J : PMF (((i : ι) → β i) × V)) (hJ : PMF.map Prod.fst J = pi p) (W : Set (((i : ι) → β i) × V)) (hW : ∃ x ∈ W, x ∈ J.support) : ∑ j : ι, dist (PMF.map (fun (x : ((i : ι) → β i) × V) => x.1 j) (J.filter W hW)) (p j) ^ 2 ≤ Real.log (1 / (J.toOuterMeasure W).toReal) / 2

Raz's conditioning lemma with side information Holenstein, proof of Corollary 6. Let (u, v) be drawn from a joint distribution J whose first marginal is the product pi p, and let W be an event about (u, v). Conditioned on W, the coordinates of u move by ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖² ≤ ln (1 / Pr[W]) / 2.

theorem Cslib.Probability.PMF.dist_map_pair_bind_eq {S : Type u_2} {X : Type u_3} {Y : Type u_4} [Fintype S] [Fintype Y] (Q : PMF (S × X)) (f : X → Y) (K : S → PMF Y) : dist (PMF.map (fun (z : S × X) => (z.1, f z.2)) Q) ((PMF.map Prod.fst Q).bind fun (s : S) => PMF.map (fun (x : Y) => (s, x)) (K s)) = ∑ s : S, ((PMF.map Prod.fst Q) s).toReal * dist (PMF.map f (conditionalSnd Q s)) (K s)

Revealing the first component: the distance of (s, f x) from (s, y) with y drawn from K s is the average over s of the distance of the conditional law of f x from K s.

noncomputable def Cslib.Probability.PMF.sideJoint {ι : Type u_2} {β : ι → Type u_3} {T : Type u_4} {V : Type u_5} (μ : PMF T) (J : T → PMF (((i : ι) → β i) × V)) : PMF ((T × V) × ((i : ι) → β i))

The joint law of ((t, v), u): t drawn from μ, then (u, v) from J t.

theorem Cslib.Probability.PMF.sideJoint_apply {ι : Type u_2} {β : ι → Type u_3} {T : Type u_4} {V : Type u_5} (μ : PMF T) (J : T → PMF (((i : ι) → β i) × V)) (t : T) (v : V) (u : (i : ι) → β i) : (sideJoint μ J) ((t, v), u) = μ t * (J t) (u, v)

def Cslib.Probability.PMF.sliceEvent {ι : Type u_2} {β : ι → Type u_3} {T : Type u_4} {V : Type u_5} (W : Set ((T × V) × ((i : ι) → β i))) (t : T) (v : V) : Set (((i : ι) → β i) × V)

The pairs (u, v) that complete (t, v) to an outcome in W.

theorem Cslib.Probability.PMF.toOuterMeasure_sliceEvent_toReal {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] {T : Type u_4} {V : Type u_5} [Finite V] (J : T → PMF (((i : ι) → β i) × V)) (W : Set ((T × V) × ((i : ι) → β i))) (t : T) (v : V) : ((J t).toOuterMeasure (sliceEvent W t v)).toReal = ∑ u : (i : ι) → β i, if ((t, v), u) ∈ W then ((J t) (u, v)).toReal else 0

theorem Cslib.Probability.PMF.map_fst_filter_sideJoint_toReal {ι : Type u_2} {β : ι → Type u_3} {T : Type u_4} {V : Type u_5} [Finite ι] [∀ (i : ι), Finite (β i)] [Finite T] [Finite V] (μ : PMF T) (J : T → PMF (((i : ι) → β i) × V)) (W : Set ((T × V) × ((i : ι) → β i))) (hW : ∃ x ∈ W, x ∈ (sideJoint μ J).support) (t : T) (v : V) : ((PMF.map Prod.fst ((sideJoint μ J).filter W hW)) (t, v)).toReal = (μ t).toReal * ((J t).toOuterMeasure (sliceEvent W t v)).toReal / ((sideJoint μ J).toOuterMeasure W).toReal

The probability of (t, v) after conditioning on W is μ t · Pr_{J t}[W_{t,v}] / Pr[W].

theorem Cslib.Probability.PMF.conditionalSnd_filter_sideJoint {ι : Type u_2} {β : ι → Type u_3} {T : Type u_4} {V : Type u_5} [Finite ι] [∀ (i : ι), Finite (β i)] [Finite T] [Finite V] (μ : PMF T) (J : T → PMF (((i : ι) → β i) × V)) (W : Set ((T × V) × ((i : ι) → β i))) (hW : ∃ x ∈ W, x ∈ (sideJoint μ J).support) (t : T) (v : V) (hs : (t, v) ∈ (PMF.map Prod.fst ((sideJoint μ J).filter W hW)).support) (hWs : ∃ x ∈ sliceEvent W t v, x ∈ (J t).support) : conditionalSnd ((sideJoint μ J).filter W hW) (t, v) = PMF.map Prod.fst ((J t).filter (sliceEvent W t v) hWs)

Given (t, v), the law of u conditioned on W is the law of u under J t conditioned on the slice W_{t,v}.

theorem Cslib.Probability.PMF.sum_dist_filter_sideJoint_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] {T : Type u_4} {V : Type u_5} [Fintype T] [Fintype V] (μ : PMF T) (K : (i : ι) → T → PMF (β i)) (J : T → PMF (((i : ι) → β i) × V)) (hJ : ∀ (t : T), PMF.map Prod.fst (J t) = pi fun (i : ι) => K i t) (W : Set ((T × V) × ((i : ι) → β i))) (hW : ∃ x ∈ W, x ∈ (sideJoint μ J).support) : ∑ j : ι, dist (PMF.map (fun (z : (T × V) × ((i : ι) → β i)) => (z.1, z.2 j)) ((sideJoint μ J).filter W hW)) ((PMF.map Prod.fst ((sideJoint μ J).filter W hW)).bind fun (s : T × V) => PMF.map (fun (x : β j) => (s, x)) (K j s.1)) ≤ √(↑(Fintype.card ι) * Real.log (↑(Fintype.card V) / ((sideJoint μ J).toOuterMeasure W).toReal) / 2)

Holenstein's Corollary 6 Holenstein, Corollary 6, with the alphabet of V in place of its support under W and the divergence in nats. Draw t from μ, then the coordinates u_i independently from K i t together with side information v ((J t).map Prod.fst = pi (K · t)), and condition on an event W. Then sampling each coordinate from K j t instead, ignoring W and v, changes the law of ((t, v), u_j) little on average: ∑ⱼ ‖P_{TV Uⱼ | W} - P_{TV | W} P_{Uⱼ | T}‖ ≤ √(k · ln (|V| / Pr[W]) / 2).