Strong extraction from all blocks with one shared seed #
A strong seeded extractor applied to every block of a block source has joint seed-output error at most the number of blocks times its one-block error. The output comparison is uniform on the entire block tuple, and the same original seed is retained once.
The proof specializes shared-seed block condensation to full output entropy. It is the extraction case of the finite block argument in Chattopadhyay--Goodman--Liao, Lemma 5.5 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.block
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
[Nonempty Seed]
[Nonempty Ω]
{E : α → Seed → Ω}
{K : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
{t : ℕ}
{p : (Fin t → α) → ℝ}
(source : IsBlockSource p K)
(T : Finset (Seed × (Fin t → Ω)))
:
|weightedSeededTestProb p (fun (x : Fin t → α) (y : Seed) (i : Fin t) => E (x i) y) T - uniformSeededTestProb T| ≤ ↑t * ε
Applying a strong extractor to all blocks with one shared seed gives uniform output tuples with joint test error at most the sum of the block errors.