Conditioning a product distribution on an event

Condition independent coordinates U₁, …, U_k on an event W. Then the coordinates barely move: ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖² ≤ ln (1 / Pr[W]) / 2 (Cslib.Probability.PMF.sum_sq_dist_map_filter_pi_le). This is Raz's conditioning lemma Raz, Claim 5.1, Holenstein, Lemma 5, and it drives the coordinate selection in the proof of the parallel repetition theorem. Holenstein states it as Pr[W] ≤ 2 ^ (-∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖²) (toOuterMeasure_toReal_le_two_rpow), which follows since ln x / 2 ≤ log₂ x for x ≥ 1, and uses it through Cauchy–Schwarz in the form ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖ ≤ √(k · ln (1 / Pr[W])) (sum_dist_map_filter_pi_le).

The proof has three steps. Conditioning on W costs exactly ln (1 / Pr[W]) nats of divergence (sum_mul_log_div_filter). Divergence from a product distribution is superadditive over the coordinates (sum_sum_mul_log_div_map_le): the gap is the divergence of the joint distribution from the product of its own marginals, which is nonnegative by Gibbs' inequality. Pinsker's inequality and Cauchy–Schwarz then bound the sum of statistical distances.

Main results

• Cslib.Probability.PMF.sum_mul_log_div_filter: conditioning on W has divergence ln (1 / Pr[W]).
• Cslib.Probability.PMF.sum_sum_mul_log_div_map_le: superadditivity of divergence from a product.
• Cslib.Probability.PMF.sum_sq_dist_map_filter_pi_le: Raz's conditioning lemma.
• Cslib.Probability.PMF.toOuterMeasure_toReal_le_two_rpow: Holenstein's form Pr[W] ≤ 2 ^ (-∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖²).
• Cslib.Probability.PMF.sq_sum_dist_map_filter_pi_le, Cslib.Probability.PMF.sum_dist_map_filter_pi_le: the forms summed by Cauchy–Schwarz, ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖ ≤ √(k · ln (1 / Pr[W])).

References

• T. Holenstein, Parallel repetition: simplifications and the no-signaling case
• R. Raz, A parallel repetition theorem

theorem Cslib.Probability.PMF.sum_mul_log_div_filter {α : Type u_1} [Fintype α] (p : PMF α) (event : Set α) (hevent : ∃ a ∈ event, a ∈ p.support) : ∑ a : α, ((p.filter event hevent) a).toReal * Real.log (((p.filter event hevent) a).toReal / (p a).toReal) = Real.log (1 / (p.toOuterMeasure event).toReal)

Conditioning on an event W has divergence ln (1 / Pr[W]) from the original distribution, in nats.

theorem Cslib.Probability.PMF.sum_sum_mul_log_div_map_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] [DecidableEq ι] (P : PMF ((i : ι) → β i)) (p : (i : ι) → PMF (β i)) (h : P.support ⊆ (pi p).support) : ∑ j : ι, ∑ a : β j, ((PMF.map (fun (u : (i : ι) → β i) => u j) P) a).toReal * Real.log (((PMF.map (fun (u : (i : ι) → β i) => u j) P) a).toReal / ((p j) a).toReal) ≤ ∑ u : (i : ι) → β i, (P u).toReal * Real.log ((P u).toReal / ((pi p) u).toReal)

Superadditivity of divergence from a product. The divergences of the marginals of P from the factors p j add up to at most the divergence of P from the product pi p, in nats.

theorem Cslib.Probability.PMF.sum_sq_dist_map_filter_pi_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (p : (i : ι) → PMF (β i)) (W : Set ((i : ι) → β i)) (hW : ∃ u ∈ W, u ∈ (pi p).support) : ∑ j : ι, dist (PMF.map (fun (u : (i : ι) → β i) => u j) ((pi p).filter W hW)) (p j) ^ 2 ≤ Real.log (1 / ((pi p).toOuterMeasure W).toReal) / 2

Raz's conditioning lemma Raz, Claim 5.1, Holenstein, Lemma 5. Conditioning independent coordinates on an event W moves them little: ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖² ≤ ln (1 / Pr[W]) / 2.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_le_two_rpow {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (p : (i : ι) → PMF (β i)) (W : Set ((i : ι) → β i)) (hW : ∃ u ∈ W, u ∈ (pi p).support) : ((pi p).toOuterMeasure W).toReal ≤ 2 ^ (-∑ j : ι, dist (PMF.map (fun (u : (i : ι) → β i) => u j) ((pi p).filter W hW)) (p j) ^ 2)

Raz's conditioning lemma in the form of Holenstein, Lemma 5, (7): Pr[W] ≤ 2 ^ (-∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖²).

theorem Cslib.Probability.PMF.sq_sum_dist_map_filter_pi_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (p : (i : ι) → PMF (β i)) (W : Set ((i : ι) → β i)) (hW : ∃ u ∈ W, u ∈ (pi p).support) : (∑ j : ι, dist (PMF.map (fun (u : (i : ι) → β i) => u j) ((pi p).filter W hW)) (p j)) ^ 2 ≤ ↑(Fintype.card ι) * Real.log (1 / ((pi p).toOuterMeasure W).toReal) / 2

Raz's conditioning lemma, summed: (∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖)² ≤ k · ln (1 / Pr[W]) / 2 for k independent coordinates, by Cauchy–Schwarz.

theorem Cslib.Probability.PMF.sum_dist_map_filter_pi_le {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (p : (i : ι) → PMF (β i)) (W : Set ((i : ι) → β i)) (hW : ∃ u ∈ W, u ∈ (pi p).support) : ∑ j : ι, dist (PMF.map (fun (u : (i : ι) → β i) => u j) ((pi p).filter W hW)) (p j) ≤ √(↑(Fintype.card ι) * Real.log (1 / ((pi p).toOuterMeasure W).toReal))

Raz's conditioning lemma in the form of Holenstein, (8): ∑ⱼ ‖P_{Uⱼ | W} - P_{Uⱼ}‖ ≤ √(k · ln (1 / Pr[W])) for k independent coordinates.