Finite neighbor coverage and somewhere sampling

A neighbor map replaces each outer seed by a list of base seeds. Coverage bounds the union reached by every sufficiently large outer support. A somewhere sampler fails at an outer seed only when every candidate belongs to the test set.

These are the finite contracts used by Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Definition 3.16 and Appendix A. They do not assert an explicit construction or a polynomial-time evaluator.

noncomputable def Algebraic.Cutwidth.Extractor.neighborSet {Outer : Type u_1} {Candidate : Type u_2} {Base : Type u_3} [Fintype Candidate] (Γ : Outer → Candidate → Base) (P : Finset Outer) : Finset Base

All base seeds reached from a finite set of outer seeds.

Equations

• Algebraic.Cutwidth.Extractor.neighborSet Γ P = P.biUnion fun (y : Outer) => Finset.image (Γ y) Finset.univ

def Algebraic.Cutwidth.Extractor.NeighborCoverage {Outer : Type u_1} {Candidate : Type u_2} {Base : Type u_3} [Fintype Candidate] [Fintype Base] (Γ : Outer → Candidate → Base) (K : ℕ) (ρ : ℝ) : Prop

Every outer support of size at least K reaches a ρ fraction of base seeds.

Equations

• Algebraic.Cutwidth.Extractor.NeighborCoverage Γ K ρ = ∀ (P : Finset Outer), K ≤ P.card → ρ * ↑(Fintype.card Base) ≤ ↑(Algebraic.Cutwidth.Extractor.neighborSet Γ P).card

noncomputable def Algebraic.Cutwidth.Extractor.allHitSeeds {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Ω : Type u_4} [Fintype Outer] (S : α → Outer → Candidate → Ω) (T : Finset Ω) (x : α) : Finset Outer

Outer seeds whose every candidate output belongs to the test set.

Equations

• Algebraic.Cutwidth.Extractor.allHitSeeds S T x = {y : Outer | ∀ (z : Candidate), S x y z ∈ T}

noncomputable def Algebraic.Cutwidth.Extractor.somewhereBadInputs {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype Outer] (S : α → Outer → Candidate → Ω) (T : Finset Ω) (ε : ℝ) : Finset α

Inputs for which more than a 2ε fraction of outer seeds have all candidates in the test set.

Equations

• Algebraic.Cutwidth.Extractor.somewhereBadInputs S T ε = {x : α | 2 * ε * ↑(Fintype.card Outer) < ↑(Algebraic.Cutwidth.Extractor.allHitSeeds S T x).card}

def Algebraic.Cutwidth.Extractor.SomewhereSampler {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype Outer] [Fintype Ω] (S : α → Outer → Candidate → Ω) (L ε δ : ℝ) : Prop

Small-set sampling with a list of candidates at each outer seed, for every probability source whose point masses are at most 1 / L. The failure event counts outer seeds whose entire candidate list hits the test set.

Equations

• One or more equations did not get rendered due to their size.