Eventual validity of the actual sumset-extractor family #
Choose the scale to be the input's ceiling binary logarithm. The cubic iterated-logarithmic bounds on candidate bits and the growing depth make both sampler guards eventual. The selected entropy exponent is bounded by an exponential of a cubic iterated logarithm and is therefore sublinear. All statements concern the fixed actual construction and its unbounded candidate count.
theorem
Algebraic.Cutwidth.Extractor.Internal.sourceReductionCandidateCount_isLittleO :
(fun (n : ℕ) => ↑(sourceReductionCandidateCount (matchedBlockSeedBits (Nat.clog 2 (n + 1))))) =o[Filter.atTop] fun (n : ℕ) => ↑n
theorem
Algebraic.Cutwidth.Extractor.Internal.sourceReductionEntropy_isLittleO :
(fun (n : ℕ) => ↑(sourceReductionEntropy n (Nat.clog 2 (n + 1)))) =o[Filter.atTop] fun (n : ℕ) => ↑n
theorem
Algebraic.Cutwidth.Extractor.Internal.eventually_sourceReductionEntropy_le :
∀ᶠ (n : ℕ) in Filter.atTop, sourceReductionEntropy n (Nat.clog 2 (n + 1)) ≤ n
theorem
Algebraic.Cutwidth.Extractor.Internal.eventually_sourceReduction_guards :
∀ᶠ (n : ℕ) in Filter.atTop, have L := Nat.clog 2 (n + 1);
0 < L ∧ GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4 ∧ GammaBlockSizeGuard (matchedBlockSeedBits L)
theorem
Algebraic.Cutwidth.Extractor.Internal.eventually_sourceReductionExtractor_flat :
∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (sourceReductionExtractor n (Nat.clog 2 (n + 1)))
(2 ^ sourceReductionEntropy n (Nat.clog 2 (n + 1))) (35 / 72)