OAI/NumberTheory/TwoPoint/Circuits/CircuitSamplingException.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exceptional event is expressed by the single-hit circuits, so it can itself be approximated by Fourier truncation in the next stage.

  1. lemma OAI.TwoPointCorrelations.isolatesOne_false_iff line 13
  2. def OAI.TwoPointCorrelations.AC0Circuit.gateSamplingException line 51
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.gateSamplingException_eval line 58
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.gateSamplingException_depth line 68
  5. lemma OAI.TwoPointCorrelations.AC0Circuit.gateSamplingException_size line 83
  6. lemma OAI.TwoPointCorrelations.sampledAndPolynomial_error_detected line 104
  7. lemma OAI.TwoPointCorrelations.gateSamplingException_pointwise_probability line 120
  8. theorem OAI.TwoPointCorrelations.exists_gateSamplingException_small line 149