Unrestricted depth-three lower bound: circuit density

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

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

theorem Complexity.DepthThreeLowerBound.sign_eq_two_indicator_sub_one (b : Bool) : sign b = 2 * indicator b - 1

theorem Complexity.DepthThreeLowerBound.finiteAvg_sign {V : Type uDepth1} [Fintype V] (f : Cube V → Bool) : (finiteAvg fun (x : Cube V) => sign (f x)) = (2 * finiteAvg fun (x : Cube V) => indicator (f x)) - 1

theorem Complexity.DepthThreeLowerBound.acceptance_density_lower_of_sign_bound {V : Type uDepth1} [Fintype V] (f : Cube V → Bool) (ε : ℝ) (h : |finiteAvg fun (x : Cube V) => sign (f x)| ≤ ε) : (1 - ε) / 2 ≤ finiteAvg fun (x : Cube V) => indicator (f x)

theorem Complexity.DepthThreeLowerBound.acceptance_density_lower_of_width_correlation {V : Type uDepth1} [Fintype V] (f : Cube V → Bool) (k : ℕ) (ε : ℝ) (h : ∀ (H : CNF V), H.WidthAtMost k → |finiteAvg fun (x : Cube V) => sign (f x) * indicator (H.eval x)| ≤ ε) : (1 - ε) / 2 ≤ finiteAvg fun (x : Cube V) => indicator (f x)