Local embedding by correlated sampling

Alice holds x, Bob holds y, and (x, y) is drawn from P. They want to extend (x, y) by a common value s drawn from the kernel K (x, y), but Alice only knows a kernel KX x and Bob only knows KY y. Using correlated sampling, each samples from his own kernel with shared randomness (Cslib.Probability.CorrelatedSampling.localSample). The result (x, y, s_A, s_B) is within statistical distance 2 ε₁ + 2 ε₂ of (x, y, s, s), where ε₁ and ε₂ are the average distances of KX x and KY y from K (x, y) (dist_embed_le). With K the conditional distribution of S given (X, Y) and KX, KY the conditional distributions given X and Y, this is Holenstein's embedding lemma Holenstein, Lemma 8: (X, Y) is 1 - 2ε₁ - 2ε₂-embeddable in (XS, YS).

Main definitions

• Cslib.Probability.CorrelatedSampling.localSample: Alice and Bob sample from their own kernels with shared randomness.

Main results

• Cslib.Probability.CorrelatedSampling.dist_localSample_le: for fixed inputs, the two local samples are within 2 δ₁ + 2 δ₂ of a common sample of K (x, y).
• Cslib.Probability.CorrelatedSampling.dist_embed_le: Holenstein's embedding lemma.

References

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

def Cslib.Probability.CorrelatedSampling.embedFamily {X : Type u_1} {Y : Type u_2} {S : Type u_3} (KX : X → PMF S) (KY : Y → PMF S) (K : X × Y → PMF S) : X ⊕ Y ⊕ X × Y → PMF S

The distributions of the embedding: Alice's kernel, Bob's kernel, and the target kernel.

noncomputable def Cslib.Probability.CorrelatedSampling.localSample {X : Type u_1} {Y : Type u_2} {S : Type u_3} [Fintype X] [Fintype Y] [Fintype S] (KX : X → PMF S) (KY : Y → PMF S) (K : X × Y → PMF S) (x : X) (y : Y) : PMF (S × S)

Alice samples from KX x and Bob from KY y, with shared randomness. The target kernel K only shapes the shared randomness; neither party needs to know the other's input.

theorem Cslib.Probability.CorrelatedSampling.dist_localSample_le {X : Type u_1} {Y : Type u_2} {S : Type u_3} [Fintype X] [Fintype Y] [Fintype S] (KX : X → PMF S) (KY : Y → PMF S) (K : X × Y → PMF S) (x : X) (y : Y) : dist (localSample KX KY K x y) (PMF.map (fun (s : S) => (s, s)) (K (x, y))) ≤ 2 * dist (KX x) (K (x, y)) + 2 * dist (KY y) (K (x, y))

For fixed inputs, the two local samples are within 2 δ₁ + 2 δ₂ of a common sample of K (x, y), where δ₁ and δ₂ are the distances of KX x and KY y from K (x, y).

theorem Cslib.Probability.CorrelatedSampling.dist_embed_le {X : Type u_1} {Y : Type u_2} {S : Type u_3} [Fintype X] [Fintype Y] [Fintype S] (P : PMF (X × Y)) (KX : X → PMF S) (KY : Y → PMF S) (K : X × Y → PMF S) : dist (P.bind fun (xy : X × Y) => PMF.map (fun (x : S × S) => (xy, x)) (localSample KX KY K xy.1 xy.2)) (P.bind fun (xy : X × Y) => PMF.map (fun (x : S × S) => (xy, x)) (PMF.map (fun (s : S) => (s, s)) (K xy))) ≤ 2 * dist (P.bind fun (xy : X × Y) => PMF.map (fun (x : S) => (xy, x)) (KX xy.1)) (P.bind fun (xy : X × Y) => PMF.map (fun (x : S) => (xy, x)) (K xy)) + 2 * dist (P.bind fun (xy : X × Y) => PMF.map (fun (x : S) => (xy, x)) (KY xy.2)) (P.bind fun (xy : X × Y) => PMF.map (fun (x : S) => (xy, x)) (K xy))

Holenstein's embedding lemma Holenstein, Lemma 8. Draw (x, y) from P. If Alice and Bob sample from their own kernels with shared randomness, the result (x, y, s_A, s_B) is within statistical distance 2 ε₁ + 2 ε₂ of (x, y, s, s) with s drawn from K (x, y), where ε₁ and ε₂ are the distances of P ⊗ KX and P ⊗ KY from P ⊗ K.