Asymptotic estimates for the specified recursive family

Cslib's natural exponential-versus-polynomial theorem supplies the ceiling-log power estimate. Mathlib's natural logarithm adjunction and little-o comparison lemmas transfer it to the actual entropy and seed formulas. The finite scheduled extractor then supplies the eventual statistical guarantee.

theorem Algebraic.Cutwidth.Extractor.Internal.eventually_polylogBlockDepth_le (a : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockDepth a n ≤ polylogBlockLength n

theorem Algebraic.Cutwidth.Extractor.Internal.polylogBlockEntropy_isLittleO (a e : ℕ) : (fun (n : ℕ) => ↑(polylogBlockEntropy a e n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

theorem Algebraic.Cutwidth.Extractor.Internal.eventually_polylogBlockEntropy_le (a e : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockEntropy a e n ≤ n

theorem Algebraic.Cutwidth.Extractor.Internal.eventually_polylogBlockSeedBits_le (a e : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockSeedBits a e n ≤ 16384 * polylogBlockLength n

theorem Algebraic.Cutwidth.Extractor.Internal.card_polylogBlockSeeds (a e n : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : Fintype.card (PolylogBlockSeeds a e n) = 2 ^ polylogBlockSeedBits a e n

theorem Algebraic.Cutwidth.Extractor.Internal.polylogBlockOutputBits_bounds (a n : ℕ) : polylogBlockLength n ^ (a + 1) ≤ polylogBlockOutputBits a n ∧ polylogBlockOutputBits a n ≤ 2 ^ a * (polylogBlockLength n + 1) ^ (a + 1)

theorem Algebraic.Cutwidth.Extractor.Internal.eventually_polylogBlockExtractor (a e : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : ∀ᶠ (n : ℕ) in Filter.atTop, WeightedStrongSeededExtractor (polylogBlockExtractor a e n) (2 ^ polylogBlockEntropy a e n) (2 ^ e)⁻¹