Unrestricted depth-three lower bound: circuit quantitative #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/CircuitQuantitative.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.
theorem
Complexity.DepthThreeLowerBound.circuit_lower_bound_of_small_cnf_correlations
(d k : ℕ)
(s : ℝ)
(hs : 0 ≤ s)
(hd : 4 ≤ d)
(hk : 3 * (s + 1) * √↑d ≤ ↑k)
(f : Cube (Fin d) → Bool)
(hcorr :
∀ (H : CNF (Fin d)),
H.WidthAtMost k →
|finiteAvg fun (x : Cube (Fin d)) => sign (f x) * indicator (H.eval x)| ≤ 6 * 2 ^ (-(64 * (s + 1) * √↑d) / 16))
(C : Circuit3 (Fin d))
(hC : C.Computes f)
: