OAI/NumberTheory/TwoPoint/Bounds/DegreeThresholdCircuit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The literal degree cutoffs are depth-two monotone circuits: a large active set contains a subset of the prescribed size.

  1. def OAI.TwoPointCorrelations.AC0Circuit.disjunction line 16
  2. lemma OAI.TwoPointCorrelations.AC0Circuit.disjunction_eval line 20
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.disjunction_depth line 30
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.disjunction_size line 39
  5. def OAI.TwoPointCorrelations.degreeSubsetCircuit line 47
  6. lemma OAI.TwoPointCorrelations.degreeSubsetCircuit_eval line 50
  7. lemma OAI.TwoPointCorrelations.degreeSubsetCircuit_depth line 60
  8. lemma OAI.TwoPointCorrelations.degreeSubsetCircuit_size line 64
  9. def OAI.TwoPointCorrelations.degreeThresholdCircuit line 68
  10. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_eval line 72
  11. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_depth line 85
  12. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_size line 89
  13. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_size_le line 99
  14. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_real_eval line 107
  15. lemma OAI.TwoPointCorrelations.degreeThresholdCircuit_size_exp line 113