OAI/NumberTheory/TwoPoint/Circuits/CircuitDepthSwitching.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Iterate switching through arbitrary AND/OR circuits. Each gate pays one switching error, so the total loss is bounded by circuit size.

  1. theorem OAI.TwoPointCorrelations.FiniteLaw.average_probability_le_union line 14
  2. theorem OAI.TwoPointCorrelations.AC0Circuit.restriction_shallow line 41