Hybrid distributions for finite binary generators -- proof internals #
theorem
Complexity.BitGenerator.orientTest_false_internal
{outputLength : ℕ}
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.orientTest_true_internal
{outputLength : ℕ}
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.acceptedSeeds_compl_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.uniformAcceptanceProbability_compl_internal
{outputLength : ℕ}
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.generatedAcceptanceProbability_compl_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.exists_orientation_of_distinguishingAdvantage_internal
{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)
theorem
Complexity.BitGenerator.hybridOutput_zero_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(randomness : Fin (seedLength + outputLength) → Bool)
:
theorem
Complexity.BitGenerator.hybridOutput_outputLength_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(randomness : Fin (seedLength + outputLength) → Bool)
:
generator.hybridOutput outputLength randomness = generator (blockFst seedLength outputLength randomness)
theorem
Complexity.BitGenerator.hybridAcceptanceProbability_zero_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
:
theorem
Complexity.BitGenerator.hybridAcceptanceProbability_outputLength_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
:
generator.hybridAcceptanceProbability test outputLength = generator.generatedAcceptanceProbability test
theorem
Complexity.BitGenerator.sum_hybridGap_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
:
∑ step ∈ Finset.range outputLength, generator.hybridGap test step = generator.generatedAcceptanceProbability test - uniformAcceptanceProbability test
theorem
Complexity.BitGenerator.exists_hybridGap_ge_average_internal
{seedLength outputLength : ℕ}
(generator : BitGenerator seedLength outputLength)
(test : Finset (Fin outputLength → Bool))
{advantage : ℚ}
(houtputLength : 0 < outputLength)
(hadvantage : advantage ≤ generator.generatedAcceptanceProbability test - uniformAcceptanceProbability test)
:
theorem
Complexity.BitGenerator.exists_oriented_hybridGap_ge_average_internal
{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