Finite seeded extraction and sampling from weak sources

The sampler tests only small output sets, as in Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Definition 3.14. Its source may have any probability weights with the stated point-mass bound. The seeded extractor premise only needs uniform sources on finite supports, since the proof applies it to the full set of bad inputs.

Seed and output types are assumed nonempty by the public conversion theorems. All counts retain seed multiplicity, including repeated output values.

noncomputable def Algebraic.Cutwidth.Extractor.seedHits {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] (E : α → Seed → Ω) (T : Finset Ω) (x : α) : ℕ

Number of seeds whose output belongs to the test set, at a fixed input.

Equations

• Algebraic.Cutwidth.Extractor.seedHits E T x = {y : Seed | E x y ∈ T}.card

noncomputable def Algebraic.Cutwidth.Extractor.badInputs {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (E : α → Seed → Ω) (T : Finset Ω) (ε : ℝ) : Finset α

Inputs for which more than a 2ε fraction of seeds hit the test set.

Equations

• Algebraic.Cutwidth.Extractor.badInputs E T ε = {x : α | 2 * ε * ↑(Fintype.card Seed) < ↑(Algebraic.Cutwidth.Extractor.seedHits E T x)}

def Algebraic.Cutwidth.Extractor.FlatSeededExtractor {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) (K : ℕ) (ε : ℝ) : Prop

Seeded extraction from every uniform support of size at least K. The discrepancy for every output test is multiplied by the number of source pairs and output values, so this definition uses no division.

Equations

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

def Algebraic.Cutwidth.Extractor.Sampler {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) (L ε δ : ℝ) : Prop

Small-set sampling for every probability source with point masses at most 1 / L, expressed as L * p x ≤ 1. For positive L, this is source min-entropy at least log₂ L. The seed is uniform and independent of the source.

Equations

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