The actual amplified linear sampler

The outer word and candidate choose a seed through the actual padded Gamma extractor. The actual growing-depth matched extractor then reads the source with that seed. Its requested output prefix is completed with false bits, so the definition is total for every width. Gamma need not be linear: for each fixed outer word and candidate, only the matched extractor reads the source.

This is the source-linear sampler composition in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.4 and Appendix A, proof of Lemma 3.17: https://arxiv.org/abs/2110.12652. Finite sampling guarantees and a uniform evaluator are separate theorems about this actual map.

def Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEntropy (L d : ℕ) : ℕ

Source entropy paying the growing extractor threshold and one sampling bit.

Equations

• Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEntropy L d = 2 ^ (2 * Algebraic.Cutwidth.Extractor.growingMatchedBlockDepth d + 14) * L + 1

def Algebraic.Cutwidth.Extractor.amplifiedMatchedSampler (n L d : ℕ) (x : Fin n → Bool) (outer : Fin (8 * matchedBlockSeedBits L) → Bool) (candidate : Fin (gammaBlockSeedBudget (matchedBlockSeedBits L)) → Bool) : Fin d → Bool

The Gamma-selected matched output, truncated or false-completed to d bits.

Equations

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