Shared-seed extraction from full-entropy block witnesses

Every full-entropy block witness is uniform on its entire tuple space. The retained-seed total-variation comparison then gives the same bound on all joint seed-output tests.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedBlockTest_of_uniform_witness {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] [Nonempty Seed] [Nonempty Ω] {t : ℕ} (p : α → ℝ) (E : α → Seed → Fin t → Ω) (probability : IsProbabilityWeight p) (q : Seed → (Fin t → Ω) → ℝ) (witness : ∀ (y : Seed), IsBlockSource (q y) (Fintype.card Ω)) {δ : ℝ} (close : weightDist (weightedSeededOutput p E) (seedFamilyWeight q) ≤ δ) (T : Finset (Seed × (Fin t → Ω))) : |weightedSeededTestProb p E T - uniformSeededTestProb T| ≤ δ

theorem Algebraic.Cutwidth.Extractor.Internal.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 * ε