The finite next-bit prediction experiment -- definitions

For each background state omega, an experiment has a target bit and a test whose outcome depends on a uniformly random candidate bit. The Yao predictor returns the candidate when the test accepts and its complement when the test rejects. All three probabilities use exact uniform finite sample spaces.

def Complexity.NextBitPrediction.predictFromTest (testResult candidate : Bool) : Bool

Predict the candidate bit when the test accepts and its complement when the test rejects. This is testResult XOR candidate XOR 1.

Equations

• Complexity.NextBitPrediction.predictFromTest testResult candidate = (testResult ^^ candidate ^^ true)

noncomputable def Complexity.NextBitPrediction.candidateAcceptanceProbability {background : Type u_1} [Fintype background] (testAt : background → Bool → Bool) : ℚ

Test acceptance when the candidate bit is uniform and independent of the background state.

Equations

• Complexity.NextBitPrediction.candidateAcceptanceProbability testAt = Complexity.uniformProbability {sample : background × Bool | testAt sample.1 sample.2 = true}

noncomputable def Complexity.NextBitPrediction.targetAcceptanceProbability {background : Type u_1} [Fintype background] (target : background → Bool) (testAt : background → Bool → Bool) : ℚ

Test acceptance when the candidate is replaced by the target bit.

Equations

• Complexity.NextBitPrediction.targetAcceptanceProbability target testAt = Complexity.uniformProbability {omega : background | testAt omega (target omega) = true}

noncomputable def Complexity.NextBitPrediction.successProbability {background : Type u_1} [Fintype background] (target : background → Bool) (testAt : background → Bool → Bool) : ℚ

Probability that the test-based predictor recovers the target from a uniform independent candidate bit.

Equations

• One or more equations did not get rendered due to their size.