OAI/NumberTheory/TwoPoint/Circuits/CircuitCertificateBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Numerical bounds carried by the recursive polynomial/error-circuit construction. They retain explicit circuit dependence until the final size and depth estimates.

  1. def OAI.TwoPointCorrelations.AC0Circuit.sampleNormBound line 18
  2. def OAI.TwoPointCorrelations.AC0Circuit.exceptionSizeBound line 25
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.sampleNormBound_nonneg line 34
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.negate_indicator line 43
  5. structure OAI.TwoPointCorrelations.CircuitCertificate line 54
  6. def OAI.TwoPointCorrelations.CircuitCertificate.literal line 66