Local embeddings

A distribution P₀ of pairs (x, y) is ε-embeddable in a distribution P₁ of ((x, y), (s, t)) Holenstein, Definition 7 if Alice, who holds x, and Bob, who holds y, can use shared randomness, but no communication, to produce s and t so that ((x, y), (s, t)) is within statistical distance ε of P₁ (Cslib.Probability.CorrelatedSampling.IsEmbeddable).

• Lemma 8 (isEmbeddable_diag): a joint distribution J of ((x, y), s) embeds its marginal in ((x, y), (s, s)) with error 2 ε₁ + 2 ε₂, where ε₁ and ε₂ are the distances of J from P_{XY} P_{S | X} and P_{XY} P_{S | Y}. This is the local embedding lemma of Complexity/Probability/CorrelatedSampling/Embedding.lean with the conditional distributions of J as kernels.
• Corollary 9 (isEmbeddable_diag_of_dist_le): the same holds for another input distribution P₀, measured by the distances of J from P₀ P_{S | X} and P₀ P_{S | Y}, with error 7 ε₁ + 2 ε₂. Holenstein states the constant 3 ε₁ + 2 ε₂; the proof here goes through the triangle inequality and the constant is this file's own.
• Lemma 10 (isEmbeddable_bind_prod): if s depends only on x and t only on y, the embedding is exact, by private randomness simulated with shared randomness.
• Fact 11 (dist_filter_le_two_mul): conditioning two distributions on an event of probability 1 / 2 under both at most doubles their distance.

Main definitions

• Cslib.Probability.CorrelatedSampling.IsEmbeddable: local embeddability.

Main results

• Cslib.Probability.CorrelatedSampling.isEmbeddable_diag: Lemma 8.
• Cslib.Probability.CorrelatedSampling.isEmbeddable_diag_of_dist_le: Corollary 9.
• Cslib.Probability.CorrelatedSampling.isEmbeddable_bind_prod: Lemma 10.
• Cslib.Probability.CorrelatedSampling.dist_filter_le_two_mul: Fact 11.

References

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

def Cslib.Probability.CorrelatedSampling.IsEmbeddable {X Y S T : Type} [Fintype X] [Fintype Y] [Fintype S] [Fintype T] (P₀ : PMF (X × Y)) (P₁ : PMF ((X × Y) × S × T)) (ε : ℝ) : Prop

Local embeddability Holenstein, Definition 7: from (x, y) drawn from P₀, Alice and Bob produce s = fA x r and t = fB y r from shared randomness r ~ ρ so that ((x, y), (s, t)) is within statistical distance ε of P₁.

noncomputable def Cslib.Probability.CorrelatedSampling.condX {X Y S : Type} (J : PMF ((X × Y) × S)) : X → PMF S

The conditional law of s given x under a joint law J of ((x, y), s).

noncomputable def Cslib.Probability.CorrelatedSampling.condY {X Y S : Type} (J : PMF ((X × Y) × S)) : Y → PMF S

The conditional law of s given y under a joint law J of ((x, y), s).

@[reducible, inline]

noncomputable abbrev Cslib.Probability.CorrelatedSampling.withKernel {X Y S : Type} (P : PMF (X × Y)) (K : X × Y → PMF S) : PMF ((X × Y) × S)

The joint law P ⊗ K of ((x, y), s) with (x, y) ~ P and s ~ K (x, y).

theorem Cslib.Probability.CorrelatedSampling.isEmbeddable_withKernel {X Y S : Type} [Fintype X] [Fintype Y] [Fintype S] (P₀ : PMF (X × Y)) (KX : X → PMF S) (KY : Y → PMF S) (K : X × Y → PMF S) : IsEmbeddable P₀ (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 (withKernel P₀ fun (xy : X × Y) => KX xy.1) (withKernel P₀ K) + 2 * dist (withKernel P₀ fun (xy : X × Y) => KY xy.2) (withKernel P₀ K))

The local embedding protocol on inputs from any P₀: its output is within 2 d(P₀ ⊗ KX, P₀ ⊗ K) + 2 d(P₀ ⊗ KY, P₀ ⊗ K) of P₀ ⊗ (K, K).

theorem Cslib.Probability.CorrelatedSampling.isEmbeddable_diag {X Y S : Type} [Fintype X] [Fintype Y] [Fintype S] (J : PMF ((X × Y) × S)) : IsEmbeddable (PMF.map Prod.fst J) (PMF.map (fun (z : (X × Y) × S) => (z.1, z.2, z.2)) J) (2 * dist J (withKernel (PMF.map Prod.fst J) fun (xy : X × Y) => condX J xy.1) + 2 * dist J (withKernel (PMF.map Prod.fst J) fun (xy : X × Y) => condY J xy.2))

Holenstein's Lemma 8 Holenstein, Lemma 8: a joint law J of ((x, y), s) embeds its marginal in ((x, y), (s, s)) with error 2 ε₁ + 2 ε₂, where ε₁ and ε₂ are the distances of J from P_{XY} P_{S | X} and P_{XY} P_{S | Y}.

theorem Cslib.Probability.CorrelatedSampling.isEmbeddable_diag_of_dist_le {X Y S : Type} [Fintype X] [Fintype Y] [Fintype S] (J : PMF ((X × Y) × S)) (P₀ : PMF (X × Y)) {ε₁ ε₂ : ℝ} (h₁ : dist J (withKernel P₀ fun (xy : X × Y) => condX J xy.1) ≤ ε₁) (h₂ : dist J (withKernel P₀ fun (xy : X × Y) => condY J xy.2) ≤ ε₂) : IsEmbeddable P₀ (PMF.map (fun (z : (X × Y) × S) => (z.1, z.2, z.2)) J) (7 * ε₁ + 2 * ε₂)

Holenstein's Corollary 9 Holenstein, Corollary 9, with the constant 7 ε₁ + 2 ε₂ of this proof: if J is within ε₁ of P₀ P_{S | X} and within ε₂ of P₀ P_{S | Y}, then P₀ embeds in ((x, y), (s, s)) under J with error 7 ε₁ + 2 ε₂.

theorem Cslib.Probability.CorrelatedSampling.isEmbeddable_bind_prod {X Y S T : Type} [Fintype X] [Fintype Y] [Fintype S] [Fintype T] (P₀ : PMF (X × Y)) (KS : X → PMF S) (KT : Y → PMF T) : IsEmbeddable P₀ (P₀.bind fun (xy : X × Y) => (KS xy.1).bind fun (s : S) => PMF.map (fun (t : T) => (xy, s, t)) (KT xy.2)) 0

Holenstein's Lemma 10 Holenstein, Lemma 10, for the factorized law it characterizes: if s is drawn from KS x and t from KT y, independently, then P₀ embeds exactly. Shared randomness simulates the private coins: it draws a random function for each party.

theorem Cslib.Probability.CorrelatedSampling.dist_filter_le_two_mul {Z : Type u_1} [Fintype Z] (p q : PMF Z) (E : Set Z) (hp : (p.toOuterMeasure E).toReal = 1 / 2) (hq : (q.toOuterMeasure E).toReal = 1 / 2) (hpE : ∃ a ∈ E, a ∈ p.support) (hqE : ∃ a ∈ E, a ∈ q.support) : dist (p.filter E hpE) (q.filter E hqE) ≤ 2 * dist p q

Holenstein's Fact 11 Holenstein, Fact 11: conditioning two distributions on an event of probability 1 / 2 under both at most doubles their statistical distance.