Final extraction after a retained-seed approximation #
Full-entropy block witnesses are uniform. Averaging the shared-seed block extraction bound over the earlier seed gives an ideal final joint law close to uniform. A previous joint approximation error survives adding the fresh independent seed and applying the extractor by distance contraction.
This is finite statistical composition of the shared-seed 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.Internal.weightedStrongSeededExtractor_retained_block
{Earlier : Type u_1}
{Fresh : Type u_2}
{α : Type u_3}
{Ω : Type u_4}
[Fintype Earlier]
[Fintype Fresh]
[Fintype α]
[Fintype Ω]
[Nonempty Earlier]
[Nonempty Fresh]
[Nonempty Ω]
{E : α → Fresh → Ω}
{K t : ℕ}
{ε η : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(p : Earlier → (Fin t → α) → ℝ)
(actual : Earlier × (Fin t → α) → ℝ)
(source : ∀ (y : Earlier), IsBlockSource (p y) K)
(close : weightDist actual (seedFamilyWeight p) ≤ η)
:
weightDist (retainedSeedStep (fun (x : Earlier) (x_1 : Fin t → α) (y : Fresh) (i : Fin t) => E (x_1 i) y) actual)
(uniformWeight ((Earlier × Fresh) × (Fin t → Ω))) ≤ η + ↑t * ε
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_retained_block_tests
{Earlier : Type u_1}
{Fresh : Type u_2}
{α : Type u_3}
{Ω : Type u_4}
[Fintype Earlier]
[Fintype Fresh]
[Fintype α]
[Fintype Ω]
[Nonempty Earlier]
[Nonempty Fresh]
[Nonempty Ω]
{E : α → Fresh → Ω}
{K t : ℕ}
{ε η : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(p : Earlier → (Fin t → α) → ℝ)
(actual : Earlier × (Fin t → α) → ℝ)
(probability : IsProbabilityWeight actual)
(source : ∀ (y : Earlier), IsBlockSource (p y) K)
(close : weightDist actual (seedFamilyWeight p) ≤ η)
(T : Finset ((Earlier × Fresh) × (Fin t → Ω)))
:
|weightTestProb (retainedSeedStep (fun (x : Earlier) (x_1 : Fin t → α) (y : Fresh) (i : Fin t) => E (x_1 i) y) actual)
T - uniformSeededTestProb T| ≤ η + ↑t * ε