OAI/NumberTheory/TwoPoint/Circuits/CircuitRecursiveApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The recursive polynomial approximation in Braverman's Lemma 8, with an explicit degree and an error union bound over the circuit tree.

  1. theorem OAI.TwoPointCorrelations.AC0Circuit.exists_polynomial_approximation line 13