OAI/NumberTheory/TwoPoint/Circuits/CircuitErrorCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The algebraic error-cutoff step of Braverman's Lemma 10. A Fourier approximation of the exceptional event suppresses the large polynomial values on that event while preserving exact zeros.

  1. def OAI.TwoPointCorrelations.exceptionalExtension line 13
  2. def OAI.TwoPointCorrelations.errorCutoffPolynomial line 17
  3. lemma OAI.TwoPointCorrelations.exceptionalExtension_boolean line 20
  4. lemma OAI.TwoPointCorrelations.errorCutoffPolynomial_zero line 28
  5. lemma OAI.TwoPointCorrelations.errorCutoffPolynomial_degree line 37
  6. lemma OAI.TwoPointCorrelations.errorCutoffPolynomial_sq_bound line 42
  7. theorem OAI.TwoPointCorrelations.errorCutoffPolynomial_mean_sq line 66