OAI/NumberTheory/TwoPoint/Circuits/CircuitGateComposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recursive use of the sampled gate polynomial. Errors in the child polynomials are charged by a finite union bound, in addition to the new gate's sampling error.

  1. theorem OAI.TwoPointCorrelations.exists_composed_and_approximation line 15