Conservative bounds at bounded recursion depth

The logarithm in the exact scheduled seed bound is at most its argument minus one. Bounding the depth and local error by the common width then gives a linear seed bound. The two entropy estimates unfold the actual reserve and recursive entropy functions.

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockSeedBits_boundedDepth_le (n L E h : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (room : 64 ≤ L) (depth : h ≤ 64) (error : E ≤ L) : scheduledBlockSeedBits n h (recursiveBlockReserve L E) E L ≤ 2 ^ 24 * L

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_depth24_le (L E : ℕ) (positive : 1 ≤ L) (error : E ≤ L) : recursiveBlockEntropy 24 (recursiveBlockReserve L E) 0 ≤ 2 ^ 62 * L

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_depth64_le (L E : ℕ) (positive : 1 ≤ L) (error : E ≤ L) : recursiveBlockEntropy 64 (recursiveBlockReserve L E) 0 ≤ 2 ^ 142 * L