OAI/NumberTheory/TwoPoint/Circuits/CircuitDyadicSampling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Only logarithmically many Bernoulli parameters are needed to isolate a zero among the inputs of an AND gate. The success constant 1/8 is sufficient for the application's unspecified absolute circuit constants.

  1. lemma OAI.TwoPointCorrelations.exists_dyadic_single_hit line 12