Correlated sampling

Two parties hold distributions P and Q on a finite set and share randomness, but do not communicate. Correlated sampling lets each party output a sample with exactly its own distribution so that the two samples agree with probability at least (1 - δ) / (1 + δ) ≥ 1 - 2δ, where δ is the statistical distance between P and Q. This is the sampling step of Holenstein's proof of the parallel repetition theorem Holenstein, Lemma 8.

Holenstein's parties scan a shared infinite sequence of uniform points of S × [0, 1] and output the first point under the graph of their own distribution. We use a finite version of the same idea. For a finite family P : I → PMF S, the region under the graph of each P i is a union of finitely many cells (Cslib.Probability.CorrelatedSampling.Cell): above each s, the intervals between consecutive values P i s. The shared randomness orders the cells by drawing them without replacement, each draw proportional to the length of the cell (weightedOrder). In such an order the first cell inside any region is distributed as a single draw from that region (map_firstIn_weightedOrder). Party i outputs the point s of the first cell under the graph of P i (sample), so its output has distribution P i (map_sample). If the first cell under the graph of P i ⊔ P j lies under the graph of P i ⊓ P j, both parties output it, which gives the agreement bound (agree_ge, disagree_le).

The finite construction of the shared randomness is an adaptation of Holenstein's argument; it proves the same bound.

Main definitions

• Cslib.Probability.CorrelatedSampling.weightedOrder: drawing all elements of a finite type without replacement, each draw proportional to a weight.
• Cslib.Probability.CorrelatedSampling.shared: the shared randomness of correlated sampling.
• Cslib.Probability.CorrelatedSampling.sample: the output of party i.

Main results

• Cslib.Probability.CorrelatedSampling.map_firstIn_weightedOrder: the first element of a set in a weighted order is a weighted draw from that set.
• Cslib.Probability.CorrelatedSampling.map_sample: party i outputs a sample of P i.
• Cslib.Probability.CorrelatedSampling.agree_ge: the two outputs agree with probability at least (1 - δ) / (1 + δ).
• Cslib.Probability.CorrelatedSampling.disagree_le: they disagree with probability at most 2δ.

References

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

Weighted orders

noncomputable def Cslib.Probability.CorrelatedSampling.weightedDraw {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) (U : Finset Ω) (hU : ∑ a ∈ U, ↑(w a) ≠ 0) : PMF Ω

One element of U, drawn with probability proportional to the weight w.

theorem Cslib.Probability.CorrelatedSampling.weightedDraw_apply {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) (U : Finset Ω) (hU : ∑ a ∈ U, ↑(w a) ≠ 0) (a : Ω) : (weightedDraw w U hU) a = if a ∈ U then ↑(w a) * (∑ b ∈ U, ↑(w b))⁻¹ else 0

noncomputable def Cslib.Probability.CorrelatedSampling.weightedOrderAux {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) : ℕ → Finset Ω → PMF (List Ω)

The first m draws without replacement from U, each proportional to w, stopping early when the remaining elements have weight zero.

noncomputable def Cslib.Probability.CorrelatedSampling.weightedOrder {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) : PMF (List Ω)

All elements of positive weight, drawn without replacement, each draw with probability proportional to the weight w.

def Cslib.Probability.CorrelatedSampling.firstIn {Ω : Type u_1} [DecidableEq Ω] (R : Finset Ω) (l : List Ω) : Option Ω

The first element of the list l that lies in R.

theorem Cslib.Probability.CorrelatedSampling.firstIn_cons {Ω : Type u_1} [DecidableEq Ω] (R : Finset Ω) (a : Ω) (l : List Ω) : firstIn R (a :: l) = if a ∈ R then some a else firstIn R l

theorem Cslib.Probability.CorrelatedSampling.firstIn_of_firstIn_union {Ω : Type u_1} [DecidableEq Ω] {A B : Finset Ω} {l : List Ω} {c : Ω} (h : firstIn (A ∪ B) l = some c) (hc : c ∈ A) : firstIn A l = some c

If the first element of l in A ∪ B lies in A, it is also the first element in A.

theorem Cslib.Probability.CorrelatedSampling.map_firstIn_weightedOrderAux {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) (m : ℕ) (U R : Finset Ω) : U.card ≤ m → ∀ (hR : ∑ a ∈ R ∩ U, ↑(w a) ≠ 0), PMF.map (firstIn R) (weightedOrderAux w m U) = PMF.map some (weightedDraw w (R ∩ U) hR)

Luce's choice axiom for weighted orders. In the draws without replacement from U, the first element of R is distributed as a single weighted draw from R ∩ U.

theorem Cslib.Probability.CorrelatedSampling.map_firstIn_weightedOrder {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (w : Ω → NNReal) (R : Finset Ω) (hR : ∑ a ∈ R, ↑(w a) ≠ 0) : PMF.map (firstIn R) (weightedOrder w) = PMF.map some (weightedDraw w R hR)

In a weighted order of all elements, the first element of R is distributed as a single weighted draw from R.

Cells

noncomputable def Cslib.Probability.CorrelatedSampling.predIn (T : Finset NNReal) (v : NNReal) : NNReal

The largest element of T below v, or 0 if there is none.

theorem Cslib.Probability.CorrelatedSampling.sum_sub_predIn (T : Finset NNReal) : ∑ v ∈ T, (v - predIn T v) = T.sup id

The gaps between consecutive elements of T add up to its maximum.

theorem Cslib.Probability.CorrelatedSampling.sum_filter_le_sub_predIn {T : Finset NNReal} {p : NNReal} (hp : p ∈ T) : ∑ v ∈ T with v ≤ p, (v - predIn T v) = p

The gaps between consecutive elements of T up to p ∈ T add up to p.

noncomputable def Cslib.Probability.CorrelatedSampling.values {S : Type u_1} {I : Type u_2} [Fintype I] (P : I → PMF S) (s : S) : Finset NNReal

The values P i s of the family at s.

@[reducible, inline]

abbrev Cslib.Probability.CorrelatedSampling.Cell {S : Type u_1} {I : Type u_2} [Fintype I] (P : I → PMF S) : Type u_1

The cells of the family: a cell ⟨s, v⟩ stands for the interval from the next smaller value at s up to the value v.

@[instance_reducible]

noncomputable instance Cslib.Probability.CorrelatedSampling.instDecidableEqCell {S : Type u_1} {I : Type u_2} [Fintype I] (P : I → PMF S) : DecidableEq (Cell P)

noncomputable def Cslib.Probability.CorrelatedSampling.weight {S : Type u_1} {I : Type u_2} [Fintype I] (P : I → PMF S) (c : Cell P) : NNReal

The length of the interval of a cell.

noncomputable def Cslib.Probability.CorrelatedSampling.under {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] (P : I → PMF S) (t : S → NNReal) : Finset (Cell P)

The cells under the graph of t.

noncomputable def Cslib.Probability.CorrelatedSampling.region {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] (P : I → PMF S) (i : I) : Finset (Cell P)

The cells under the graph of P i.

noncomputable def Cslib.Probability.CorrelatedSampling.shared {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] (P : I → PMF S) : PMF (List (Cell P))

The shared randomness of correlated sampling: a weighted order of the cells.

noncomputable def Cslib.Probability.CorrelatedSampling.sample {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] (P : I → PMF S) (i : I) (l : List (Cell P)) : S

The output of party i: the point of the first cell under the graph of P i.

theorem Cslib.Probability.CorrelatedSampling.mem_values {S : Type u_1} {I : Type u_2} [Fintype I] {P : I → PMF S} (i : I) (s : S) : ((P i) s).toNNReal ∈ values P s

theorem Cslib.Probability.CorrelatedSampling.sum_weight_fiber {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} [DecidableEq S] {t : S → NNReal} (s : S) (hts : t s ∈ values P s) : ∑ c ∈ under P t with c.fst = s, weight P c = t s

Above each point, the cells under the graph of t have total length t s.

theorem Cslib.Probability.CorrelatedSampling.sum_weight_under {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} {t : S → NNReal} (ht : ∀ (s : S), t s ∈ values P s) : ∑ c ∈ under P t, weight P c = ∑ s : S, t s

The cells under the graph of t have total length ∑ s, t s.

theorem Cslib.Probability.CorrelatedSampling.under_inter_under {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (t t' : S → NNReal) : under P t ∩ under P t' = under P (t ⊓ t')

theorem Cslib.Probability.CorrelatedSampling.under_union_under {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (t t' : S → NNReal) : under P t ∪ under P t' = under P (t ⊔ t')

theorem Cslib.Probability.CorrelatedSampling.coe_toNNReal_apply {S : Type u_1} {I : Type u_2} {P : I → PMF S} (i : I) (s : S) : ↑((P i) s).toNNReal = (P i) s

theorem Cslib.Probability.CorrelatedSampling.sum_weight_region {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i : I) : ∑ c ∈ region P i, ↑(weight P c) = 1

The region of each party has total length one.

theorem Cslib.Probability.CorrelatedSampling.sum_weight_region_ne_zero {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i : I) : ∑ c ∈ region P i, ↑(weight P c) ≠ 0

theorem Cslib.Probability.CorrelatedSampling.map_sample {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i : I) : PMF.map (sample P i) (shared P) = P i

Correlated sampling, marginals. Party i outputs a sample of P i.

theorem Cslib.Probability.CorrelatedSampling.toOuterMeasure_firstIn_union {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i j : I) : (shared P).toOuterMeasure (firstIn (region P i ∪ region P j) ⁻¹' some '' ↑(region P i ∩ region P j)) = (∑ c ∈ region P i ∩ region P j, ↑(weight P c)) * (∑ c ∈ region P i ∪ region P j, ↑(weight P c))⁻¹

The probability that the first cell under the graph of P i ⊔ P j lies under the graph of P i ⊓ P j: the ratio of the lengths of the two regions.

theorem Cslib.Probability.CorrelatedSampling.sum_weight_region_inter {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i j : I) : ∑ c ∈ region P i ∩ region P j, weight P c = ∑ s : S, min ((P i) s).toNNReal ((P j) s).toNNReal

The regions of two parties meet in length ∑ s, min (P i s) (P j s) and together have length ∑ s, max (P i s) (P j s).

theorem Cslib.Probability.CorrelatedSampling.sum_weight_region_union {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i j : I) : ∑ c ∈ region P i ∪ region P j, weight P c = ∑ s : S, max ((P i) s).toNNReal ((P j) s).toNNReal

theorem Cslib.Probability.CorrelatedSampling.agree_ge {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i j : I) : (1 - dist (P i) (P j)) / (1 + dist (P i) (P j)) ≤ ((shared P).toOuterMeasure {l : List (Cell P) | sample P i l = sample P j l}).toReal

Correlated sampling Holenstein, proof of Lemma 8. The outputs of parties i and j agree with probability at least (1 - δ) / (1 + δ), where δ is the statistical distance between P i and P j.

theorem Cslib.Probability.CorrelatedSampling.disagree_le {S : Type u_1} {I : Type u_2} [Fintype S] [Fintype I] {P : I → PMF S} (i j : I) : ((shared P).toOuterMeasure {l : List (Cell P) | sample P i l ≠ sample P j l}).toReal ≤ 2 * dist (P i) (P j)

Correlated sampling, disagreement. The outputs of parties i and j differ with probability at most 2δ / (1 + δ) ≤ 2δ, where δ is the statistical distance between P i and P j.