Hybrid distributions for finite binary generators

This module gives the exact finite hybrid argument used at the start of the Nisan--Wigderson reconstruction. The zero hybrid is uniform, the final hybrid is the generator distribution, and the adjacent gaps telescope. Consequently, any positive absolute distinguishing advantage can be oriented by optionally complementing the test, after which one adjacent hybrid gap is at least the advantage divided by the output length.

@[simp]

theorem Complexity.BitGenerator.orientTest_false {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) : orientTest test false = test

@[simp]

theorem Complexity.BitGenerator.orientTest_true {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) : orientTest test true = testᶜ

theorem Complexity.BitGenerator.acceptedSeeds_compl {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : generator.acceptedSeeds testᶜ = (generator.acceptedSeeds test)ᶜ

Accepted seeds for the complementary test are exactly the complement of the accepted-seed event.

theorem Complexity.BitGenerator.uniformAcceptanceProbability_compl {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) : uniformAcceptanceProbability testᶜ = 1 - uniformAcceptanceProbability test

Complementing a test complements its uniform acceptance probability.

theorem Complexity.BitGenerator.generatedAcceptanceProbability_compl {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : generator.generatedAcceptanceProbability testᶜ = 1 - generator.generatedAcceptanceProbability test

Complementing a test complements its generated acceptance probability.

theorem Complexity.BitGenerator.exists_orientation_of_distinguishingAdvantage {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) {advantage : ℚ} (hadvantage : advantage ≤ generator.distinguishingAdvantage test) : ∃ (complement : Bool), advantage ≤ generator.generatedAcceptanceProbability (orientTest test complement) - uniformAcceptanceProbability (orientTest test complement)

One polarity of a test realizes its absolute distinguishing advantage as an oriented generated-minus-uniform gap.

theorem Complexity.BitGenerator.hybridOutput_zero {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (randomness : Fin (seedLength + outputLength) → Bool) : generator.hybridOutput 0 randomness = blockSnd seedLength outputLength randomness

The zero hybrid is exactly the independent uniform-output block.

theorem Complexity.BitGenerator.hybridOutput_outputLength {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (randomness : Fin (seedLength + outputLength) → Bool) : generator.hybridOutput outputLength randomness = generator (blockFst seedLength outputLength randomness)

The final hybrid is exactly the generator output.

theorem Complexity.BitGenerator.hybridAcceptanceProbability_zero {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : generator.hybridAcceptanceProbability test 0 = uniformAcceptanceProbability test

Test acceptance on the zero hybrid is its uniform acceptance probability.

theorem Complexity.BitGenerator.hybridAcceptanceProbability_outputLength {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : generator.hybridAcceptanceProbability test outputLength = generator.generatedAcceptanceProbability test

Test acceptance on the final hybrid is its generated acceptance probability.

theorem Complexity.BitGenerator.sum_hybridGap {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : ∑ step ∈ Finset.range outputLength, generator.hybridGap test step = generator.generatedAcceptanceProbability test - uniformAcceptanceProbability test

Adjacent hybrid gaps telescope exactly to the oriented distinguishing gap between generated and uniform outputs.

theorem Complexity.BitGenerator.exists_hybridGap_ge_average {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) {advantage : ℚ} (houtputLength : 0 < outputLength) (hadvantage : advantage ≤ generator.generatedAcceptanceProbability test - uniformAcceptanceProbability test) : ∃ step < outputLength, advantage / ↑outputLength ≤ generator.hybridGap test step

If the oriented distinguishing gap is at least advantage, one adjacent hybrid gap is at least advantage / outputLength.

theorem Complexity.BitGenerator.exists_oriented_hybridGap_ge_average {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) {advantage : ℚ} (houtputLength : 0 < outputLength) (hadvantage : advantage ≤ generator.distinguishingAdvantage test) : ∃ (complement : Bool), ∃ step < outputLength, advantage / ↑outputLength ≤ generator.hybridGap (orientTest test complement) step

Finite Yao hybrid step: every absolute distinguishing advantage admits a polarity and an adjacent hybrid whose gap is at least the average advantage.