Finite statistical tests for binary generators -- proof internals

The central fact is disjointness: a test containing only strings of complexity at least threshold cannot accept an output whose complexity is strictly below threshold. Exact zero generated mass and the density-to-advantage bound then follow by finite counting.

theorem Complexity.BitGenerator.isTimeBoundedRandomTest_iff_subset_internal {outputLength tapes time threshold : ℕ} {test : Finset (Fin outputLength → Bool)} {machine : TM tapes} : IsTimeBoundedRandomTest test machine time threshold ↔ test ⊆ machine.timeBoundedRandomStrings outputLength time threshold

theorem Complexity.BitGenerator.timeBoundedRandomStrings_isRandomTest_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : IsTimeBoundedRandomTest (machine.timeBoundedRandomStrings outputLength time threshold) machine time threshold

theorem Complexity.BitGenerator.timeBoundedRandomStrings_isDenseTest_internal {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : IsDenseTest (machine.timeBoundedRandomStrings outputLength time threshold) (1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength)

theorem Complexity.BitGenerator.hasLowTimeBoundedComplexity_of_seedDescriptions_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) : generator.HasLowTimeBoundedComplexity machine time threshold

theorem Complexity.BitGenerator.output_not_mem_of_randomTest_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (seed : Fin seedLength → Bool) : generator seed ∉ test

theorem Complexity.BitGenerator.acceptedSeeds_eq_empty_of_randomTest_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.acceptedSeeds test = ∅

theorem Complexity.BitGenerator.generatedAcceptanceProbability_eq_zero_of_randomTest_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.generatedAcceptanceProbability test = 0

theorem Complexity.BitGenerator.distinguishingAdvantage_eq_uniform_of_randomTest_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.distinguishingAdvantage test = uniformAcceptanceProbability test

theorem Complexity.BitGenerator.density_le_distinguishingAdvantage_of_randomTest_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (hdense : IsDenseTest test density) : density ≤ generator.distinguishingAdvantage test

theorem Complexity.BitGenerator.density_le_distinguishingAdvantage_of_seedDescriptions_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (hdense : IsDenseTest test density) : density ≤ generator.distinguishingAdvantage test

theorem Complexity.BitGenerator.incompressibilityBound_le_distinguishingAdvantage_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) : 1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ generator.distinguishingAdvantage (machine.timeBoundedRandomStrings outputLength time threshold)

theorem Complexity.BitGenerator.incompressibilityBound_le_distinguishingAdvantage_of_seedDescriptions_internal {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) : 1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ generator.distinguishingAdvantage (machine.timeBoundedRandomStrings outputLength time threshold)