Unrestricted depth-three lower bound: circuit lower bound

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/CircuitLowerBound.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

theorem Complexity.DepthThreeLowerBound.CNF.mass_le_of_width_correlation {V : Type uDepth1} [instFintypeV : Fintype V] (H : CNF V) (hH : H.Normalized) (f : Cube V → Bool) (hsupport : ∀ (x : Cube V), H.eval x = true → f x = true) (k : ℕ) (ε : ℝ) (hcorr : ∀ (J : CNF V), J.WidthAtMost k → |finiteAvg fun (x : Cube V) => sign (f x) * indicator (J.eval x)| ≤ ε) : (finiteAvg fun (x : Cube V) => indicator (H.eval x)) ≤ ε + ↑(List.length H) * (2 ^ k)⁻¹

theorem Complexity.DepthThreeLowerBound.Circuit3.indicator_output_le_sum_middle {V : Type uDepth1} (C : Circuit3 V) (x : Cube V) : indicator (C.eval x) ≤ ∑ j ∈ C.top, indicator ((C.middleCNF j).eval x)

theorem Complexity.DepthThreeLowerBound.Circuit3.acceptance_density_le {V : Type uDepth1} [instFintypeV : Fintype V] (C : Circuit3 V) (f : Cube V → Bool) (hC : C.Computes f) (k : ℕ) (ε : ℝ) (hε : 0 ≤ ε) (hcorr : ∀ (H : CNF V), H.WidthAtMost k → |finiteAvg fun (x : Cube V) => sign (f x) * indicator (H.eval x)| ≤ ε) : (finiteAvg fun (x : Cube V) => indicator (f x)) ≤ ↑C.gateCount * ε + ↑C.gateCount ^ 2 * (2 ^ k)⁻¹