Circuit interface for relative approximate counting -- proof internals #
theorem
Complexity.ApproximateCounting.Relative.badSeedEvent_eq_failureEvent_internal
{inputWidth outputWidth domainWidth internalGates precision failureBits : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit : Circuit Basis.andOr2 (seedWidth domainWidth precision failureBits + inputWidth) outputWidth internalGates}
(himplements : CircuitImplements precision failureBits setOfInput circuit)
(input : BitString inputWidth)
:
circuit.badSeedEvent (OutputIsAccurate precision setOfInput) input = failureEvent precision failureBits (setOfInput input)
theorem
Complexity.ApproximateCounting.Relative.eventProb_badSeedEvent_le_two_pow_internal
{inputWidth outputWidth domainWidth internalGates precision failureBits : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit : Circuit Basis.andOr2 (seedWidth domainWidth precision failureBits + inputWidth) outputWidth internalGates}
(hprecision : 0 < precision)
(himplements : CircuitImplements precision failureBits setOfInput circuit)
(input : BitString inputWidth)
:
eventProb (circuit.badSeedEvent (OutputIsAccurate precision setOfInput) input) ≤ 1 / 2 ^ failureBits
theorem
Complexity.ApproximateCounting.Relative.exists_hardwired_accurate_circuit_internal
{inputWidth outputWidth domainWidth internalGates precision : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit :
Circuit Basis.andOr2 (seedWidth domainWidth precision (inputWidth + 1) + inputWidth) outputWidth internalGates}
(hprecision : 0 < precision)
(himplements : CircuitImplements precision (inputWidth + 1) setOfInput circuit)
:
∃ (fixed : Circuit Basis.andOr2 inputWidth outputWidth internalGates),
(∀ (input : BitString inputWidth), OutputIsAccurate precision setOfInput input (fixed.eval input)) ∧ fixed.size = circuit.size