Amplifying a finite sampler by neighbor coverage

A large set of outer seeds reaches more base seeds than a good input can send into a test set. Therefore few outer seeds have every candidate in that test. The bad-input inclusion preserves the sampler's arbitrary source weights and its failure probability.

This is the finite reduction in Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Appendix A, proof of Lemma 3.17: https://arxiv.org/abs/2110.12652. Seeded extraction also gives the needed coverage by testing the full neighbor image. This permits a constant-error extractor to supply the neighbor map when its seed count is affordable.

The theorems prove these implications. SourceReduction.Sampler instantiates them with the padded Γ extractor as an explicit neighbor map (amplifiedMatchedSampler_somewhereSampler); its evaluator is polynomial-time (gammaBlockExtractorRuntime_mem_FP).

theorem Algebraic.Cutwidth.Extractor.NeighborCoverage.card_allHitSeeds_lt {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Base : Type u_4} {Ω : Type u_5} [Fintype Outer] [Fintype Candidate] [Fintype Base] [Nonempty Base] {Γ : Outer → Candidate → Base} {K : ℕ} {ρ ε₀ : ℝ} (cover : NeighborCoverage Γ K ρ) (separate : 2 * ε₀ < ρ) (E : α → Base → Ω) (T : Finset Ω) (x : α) (good : ↑(seedHits E T x) ≤ 2 * ε₀ * ↑(Fintype.card Base)) : (allHitSeeds (fun (x : α) (y : Outer) (z : Candidate) => E x (Γ y z)) T x).card < K

At a base-good input, fewer than K outer seeds have all candidates in the test set. The strict coverage gap remains strict because the base is nonempty.

theorem Algebraic.Cutwidth.Extractor.FlatSeededExtractor.neighborCoverage {Outer : Type u_1} {Candidate : Type u_2} {Base : Type u_3} [Fintype Candidate] [Nonempty Candidate] [Fintype Base] {Γ : Outer → Candidate → Base} {K : ℕ} {ε : ℝ} (extract : FlatSeededExtractor Γ K ε) (positive : 0 < K) : NeighborCoverage Γ K (1 - ε)

Extraction forces every large support to reach at least a 1 - ε fraction of outputs. The source support and the uniform seed are nonempty.

theorem Algebraic.Cutwidth.Extractor.Sampler.amplify {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Base : Type u_4} {Ω : Type u_5} [Fintype α] [Fintype Outer] [Fintype Candidate] [Fintype Base] [Fintype Ω] [Nonempty Base] {E : α → Base → Ω} {Γ : Outer → Candidate → Base} {K : ℕ} {L ε₀ ε δ ρ : ℝ} (sample : Sampler E L ε₀ δ) (cover : NeighborCoverage Γ K ρ) (small : ε ≤ ε₀) (separate : 2 * ε₀ < ρ) (budget : ↑K ≤ 2 * ε * ↑(Fintype.card Outer)) : SomewhereSampler (fun (x : α) (y : Outer) (z : Candidate) => E x (Γ y z)) L ε δ

Compose a sampler with a covering neighbor map. The target tests may be smaller, and the source point-mass and failure bounds are preserved exactly.

theorem Algebraic.Cutwidth.Extractor.neighborCoverage_seedProjection {Outer : Type u_1} {Base : Type u_2} [Fintype Base] {K : ℕ} (positive : 0 < K) : NeighborCoverage (fun (x : Outer) (z : Base) => z) K 1

Listing every base seed gives full coverage of every nonempty support.

theorem Algebraic.Cutwidth.Extractor.somewhereSampler_seedProjection {α : Type u_1} {Outer : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Outer] [Fintype Ω] [Nonempty Ω] {L ε : ℝ} (nonneg : 0 ≤ ε) (small : ε < 1) : SomewhereSampler (fun (x : α) (x_1 : Outer) (z : Ω) => z) L ε 0

Listing every output at each outer seed has zero failure probability for every proper-density test. This example uses as many candidates as outputs.