OAI/NumberTheory/TwoPoint/Circuits/CircuitNormBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A coarse uniform bound on the exceptional values of the polynomial. For fixed depth its logarithm is polynomial in the sampling count and log size.

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