Two-source extractors and the Chor–Goldreich theorem

A two-source extractor ext : X → Y → Output needs no seed: applied to independent samples of two sources with min-entropy at least k₁ and k₂, its output is within statistical distance ε of uniform (Cslib.Probability.IsTwoSourceExtractor). It is strong in the second source if the output stays ε-close to uniform even when the second sample is revealed (Cslib.Probability.IsStrongTwoSourceExtractor) Chor and Goldreich, Vadhan, Chapter 6.

Chor–Goldreich. The inner product modulo two of two bit strings of length n is a strong two-source extractor with error 2 ^ ((n - k₁ - k₂) / 2) / 2 (isStrongTwoSourceExtractor_dotProduct, isTwoSourceExtractor_dotProduct), from the average bias bound sum_mul_abs_bias_dotProduct_le. The error is below 1 / 2 once k₁ + k₂ > n and decays exponentially in k₁ + k₂ - n Chor and Goldreich, Theorem 9.

The statistical distance of a bit from uniform is half its bias |𝔼 (-1)^b| (dist_map_uniformOfFintype_bool). Given the revealed y, the bias of x ⬝ᵥ y is a Hadamard transform of the distribution p of x. By Cauchy–Schwarz over y and Parseval's identity for the Hadamard transform (BitString.sum_sq_sum_mul_signVal_dotProduct), the average bias is at most √(2 ^ n ‖p‖² ‖q‖²), and a source of min-entropy k has ‖p‖² ≤ 2 ^ (-k). The argument applies to every source directly, without decomposing it into flat sources.

The threshold k₁ + k₂ > n cannot be lowered to k₁ + k₂ = n: strings supported on a set S of coordinates and strings supported on its complement are orthogonal, so the inner product of uniform samples of the two is constant (exists_minEntropy_bind_dotProduct_eq_pure, not_isTwoSourceExtractor_dotProduct).

Main definitions

• Cslib.Probability.IsTwoSourceExtractor: two-source extractors.
• Cslib.Probability.IsStrongTwoSourceExtractor: two-source extractors that are strong in the second source.

Main results

• Cslib.Probability.IsStrongTwoSourceExtractor.isTwoSourceExtractor: strong two-source extractors are two-source extractors.
• Cslib.Probability.dist_map_uniformOfFintype_bool: distance of a bit from uniform is half its bias.
• Cslib.Probability.sum_mul_abs_bias_dotProduct_le: the Chor–Goldreich bias bound.
• Cslib.Probability.isStrongTwoSourceExtractor_dotProduct, Cslib.Probability.isTwoSourceExtractor_dotProduct: the Chor–Goldreich theorem.
• Cslib.Probability.exists_minEntropy_bind_dotProduct_eq_pure, Cslib.Probability.not_isTwoSourceExtractor_dotProduct: the inner product does not extract from sources with k₁ + k₂ = n.

References

• B. Chor and O. Goldreich, Unbiased bits from sources of weak randomness and probabilistic communication complexity
• S. Vadhan, Pseudorandomness, Chapter 6

def Cslib.Probability.IsTwoSourceExtractor {X : Type u_1} {Y : Type u_2} {Output : Type u_3} [Fintype Output] [Nonempty Output] (ext : X → Y → Output) (k₁ k₂ ε : ℝ) : Prop

A two-source (k₁, k₂, ε)-extractor: for independent sources of min-entropy at least k₁ and k₂, applying ext to independent samples gives an output within statistical distance ε of uniform.

def Cslib.Probability.IsStrongTwoSourceExtractor {X : Type u_1} {Y : Type u_2} {Output : Type u_3} [Fintype Output] [Nonempty Output] [Fintype Y] (ext : X → Y → Output) (k₁ k₂ ε : ℝ) : Prop

A two-source (k₁, k₂, ε)-extractor that is strong in the second source: for independent sources of min-entropy at least k₁ and k₂, the second sample paired with the output is within statistical distance ε of the second sample paired with an independent uniform output.

theorem Cslib.Probability.IsTwoSourceExtractor.mono {X : Type u_1} {Y : Type u_2} {Output : Type u_3} [Fintype Output] [Nonempty Output] {ext : X → Y → Output} {k₁ k₂ k₁' k₂' ε ε' : ℝ} (h : IsTwoSourceExtractor ext k₁ k₂ ε) (hk₁ : k₁ ≤ k₁') (hk₂ : k₂ ≤ k₂') (hε : ε ≤ ε') : IsTwoSourceExtractor ext k₁' k₂' ε'

Two-source extractors remain two-source extractors for sources with more min-entropy and with more error.

theorem Cslib.Probability.IsStrongTwoSourceExtractor.mono {X : Type u_1} {Y : Type u_2} {Output : Type u_3} [Fintype Output] [Nonempty Output] {ext : X → Y → Output} {k₁ k₂ k₁' k₂' ε ε' : ℝ} [Fintype Y] (h : IsStrongTwoSourceExtractor ext k₁ k₂ ε) (hk₁ : k₁ ≤ k₁') (hk₂ : k₂ ≤ k₂') (hε : ε ≤ ε') : IsStrongTwoSourceExtractor ext k₁' k₂' ε'

Strong two-source extractors remain strong for sources with more min-entropy and with more error.

theorem Cslib.Probability.IsStrongTwoSourceExtractor.isTwoSourceExtractor {X : Type u_1} {Y : Type u_2} {Output : Type u_3} [Fintype Output] [Nonempty Output] {ext : X → Y → Output} {k₁ k₂ ε : ℝ} [Fintype Y] (h : IsStrongTwoSourceExtractor ext k₁ k₂ ε) : IsTwoSourceExtractor ext k₁ k₂ ε

Strong two-source extractors are two-source extractors: forgetting the revealed second sample cannot increase statistical distance.

The bias of a bit

theorem Cslib.Probability.dist_map_uniformOfFintype_bool {α : Type u_4} [Fintype α] (p : PMF α) (f : α → Bool) : dist (PMF.map f p) (PMF.uniformOfFintype Bool) = |∑ a : α, (p a).toReal * BitString.signVal (f a)| / 2

Statistical distance of a bit from uniform is half its bias: for a bit f a computed from a sample a of p, the distance from a uniform bit is |𝔼 (-1)^{f a}| / 2.

The Chor–Goldreich theorem

theorem Cslib.Probability.sum_mul_abs_bias_dotProduct_le {k₁ k₂ : ℝ} {ι : Type u_4} [Fintype ι] [DecidableEq ι] {p q : PMF (ι → Bool)} (hp : k₁ ≤ PMF.minEntropy p) (hq : k₂ ≤ PMF.minEntropy q) : ∑ y : ι → Bool, (q y).toReal * |∑ x : ι → Bool, (p x).toReal * BitString.signVal (x ⬝ᵥ y)| ≤ 2 ^ ((↑(Fintype.card ι) - k₁ - k₂) / 2)

The Chor–Goldreich bias bound. For independent sources p and q of bit strings indexed by ι, with n = |ι| and min-entropy at least k₁ and k₂, the bias |𝔼ₓ (-1)^{x ⬝ᵥ y}| of the inner product, averaged over y drawn from q, is at most 2 ^ ((n - k₁ - k₂) / 2).

theorem Cslib.Probability.isStrongTwoSourceExtractor_dotProduct {ι : Type u_4} [Fintype ι] [DecidableEq ι] (k₁ k₂ : ℝ) : IsStrongTwoSourceExtractor (fun (x y : ι → Bool) => x ⬝ᵥ y) k₁ k₂ (2 ^ ((↑(Fintype.card ι) - k₁ - k₂) / 2) / 2)

The Chor–Goldreich theorem, strong form. The inner product modulo two of bit strings indexed by ι, with n = |ι|, is a two-source extractor strong in the second source: for independent sources of min-entropy at least k₁ and k₂, revealing the second sample leaves the inner product within statistical distance 2 ^ ((n - k₁ - k₂) / 2) / 2 of a uniform bit.

theorem Cslib.Probability.isTwoSourceExtractor_dotProduct {ι : Type u_4} [Fintype ι] (k₁ k₂ : ℝ) : IsTwoSourceExtractor (fun (x y : ι → Bool) => x ⬝ᵥ y) k₁ k₂ (2 ^ ((↑(Fintype.card ι) - k₁ - k₂) / 2) / 2)

The Chor–Goldreich theorem. The inner product modulo two of bit strings indexed by ι, with n = |ι|, is a two-source extractor for min-entropies k₁ and k₂ with error 2 ^ ((n - k₁ - k₂) / 2) / 2.

The entropy threshold is necessary

theorem Cslib.Probability.exists_minEntropy_bind_dotProduct_eq_pure {ι : Type u_4} [Fintype ι] [DecidableEq ι] (S : Finset ι) : ∃ (p : PMF (ι → Bool)) (q : PMF (ι → Bool)), PMF.minEntropy p = ↑S.card ∧ PMF.minEntropy q = ↑Sᶜ.card ∧ (p.bind fun (x : ι → Bool) => PMF.map (fun (y : ι → Bool) => x ⬝ᵥ y) q) = PMF.pure false

Orthogonal sources. For every set S of coordinates, the uniform distributions on the strings vanishing outside S and on those vanishing on S have min-entropy |S| and |Sᶜ|, whose sum is n, yet the inner product of independent samples is always false.

theorem Cslib.Probability.not_isTwoSourceExtractor_dotProduct {ε : ℝ} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (S : Finset ι) (hε : ε < 1 / 2) : ¬IsTwoSourceExtractor (fun (x y : ι → Bool) => x ⬝ᵥ y) (↑S.card) (↑Sᶜ.card) ε

The threshold k₁ + k₂ > n is necessary. For every set S of coordinates, the inner product is not a two-source extractor for min-entropies |S| and |Sᶜ|, which sum to n, with error less than 1 / 2 (exists_minEntropy_bind_dotProduct_eq_pure).