OAI/NumberTheory/TwoPoint/Circuits/CircuitSampleNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise norm bounds for the sampled polynomial. These control the exceptional values when the Fourier approximation is used as a cutoff.

  1. lemma OAI.TwoPointCorrelations.andGateFactor_abs_le line 13
  2. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_abs_le line 33