The threshold of the explicit affine disperser

The explicit disperser on N bits is nonconstant on affine subspaces of dimension greater than explicitThreshold N. With ℓ = ⌊log₂ N⌋, L = ⌊ℓ / 3⌋ and n, r, s, t as in Cslib.AffineDisperser.explicitThreshold, every term is at most a constant times N / (ℓ + 1), except 2 r (r + 1), which is small because n is large:

• the unread bits number N - r n < n ≤ N / (ℓ + 1) ^ 2, and n t, ⌊n r / t⌋ ≤ N / (ℓ + 1);
• the subfield term is r s ≤ N / (L + 1) ≤ 3 N / (ℓ + 1);
• either the greedy choice of primes stops within a factor 4 L of its budget N / (ℓ + 1) ^ 2, and then r < 2 (ℓ + 1) ^ 3, or it takes every prime in (L, 4 L], whose product is at least 4 ^ L / (4 L + 1) ^ (4 ⌊√L⌋ + 5) ≥ √(8 (ℓ + 1) N) for large N by Chebyshev's bounds.

Hence (ℓ + 1) * explicitThreshold N ≤ 6 N for all large N (Cslib.AffineDisperser.eventually_explicitThreshold_le), and the threshold is O(N / log N).

Main results

• Cslib.AffineDisperser.eventually_explicitThreshold_le: (⌊log₂ N⌋ + 1) * explicitThreshold N ≤ 6 N for all large N.
• Cslib.AffineDisperser.eventually_explicitThreshold_lt: explicitThreshold N < N for all large N, so the disperser theorem is not vacuous.
• Cslib.AffineDisperser.isBigO_explicitThreshold: explicitThreshold N = O(N / log N).

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials
• P. L. Chebyshev, Mémoire sur les nombres premiers

theorem Cslib.AffineDisperser.eventually_explicitThreshold_le : ∀ᶠ (N : ℕ) in Filter.atTop, (Nat.log 2 N + 1) * explicitThreshold N ≤ 6 * N

The threshold is O(N / log N), with the explicit constant 6: (⌊log₂ N⌋ + 1) * explicitThreshold N ≤ 6 N for all large N.

theorem Cslib.AffineDisperser.eventually_explicitThreshold_lt : ∀ᶠ (N : ℕ) in Filter.atTop, explicitThreshold N < N

The disperser theorem is not vacuous: explicitThreshold N < N for all large N.

theorem Cslib.AffineDisperser.isBigO_explicitThreshold : (fun (N : ℕ) => ↑(explicitThreshold N)) =O[Filter.atTop] fun (N : ℕ) => ↑N / Real.log ↑N

The threshold is O(N / log N).