OAI/NumberTheory/TwoPoint/Circuits/CircuitPolynomialGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The explicit dyadic independence budget is polynomial in its accuracy parameter. The closure argument avoids expanding enormous fixed constants.

  1. def OAI.TwoPointCorrelations.NatPolynomialGrowth line 10
  2. theorem OAI.TwoPointCorrelations.NatPolynomialGrowth.const line 15
  3. theorem OAI.TwoPointCorrelations.NatPolynomialGrowth.id line 18
  4. theorem OAI.TwoPointCorrelations.NatPolynomialGrowth.add line 21
  5. theorem OAI.TwoPointCorrelations.NatPolynomialGrowth.mul line 32
  6. theorem OAI.TwoPointCorrelations.NatPolynomialGrowth.pow line 41
  7. theorem OAI.TwoPointCorrelations.bravermanDegree_polynomial line 51
  8. theorem OAI.TwoPointCorrelations.bravermanDegree_polynomial_positive line 72