Unrestricted depth-three lower bound: wide correlation #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/WideCorrelation.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.
theorem
Complexity.DepthThreeLowerBound.wide_correlation_of_good_restrictions
{V : Type uDepth1}
[Fintype V]
[DecidableEq V]
{p ε : ℝ}
(hp0 : 0 < p)
(hp1 : p < 1)
(hε : 0 ≤ ε)
(b k : ℕ)
(hb : 1 ≤ b)
(hθ : restrictionTheta k b p ≤ 1 / 2)
(f : Cube V → Bool)
(hbad : (restrictionAvg p fun (σ : Restriction V) => if ¬goodRestriction p ε b f σ then 1 else 0) ≤ 4 * ε)
(H : CNF V)
: