Unrestricted depth-three lower bound: sparse correlation

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

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

theorem Complexity.DepthThreeLowerBound.SparsePartition.correlation_eq_sum {V : Type u} [Fintype V] {H : CNF V} {b M : ℕ} {η : ℝ} (P : SparsePartition H b M η) (G : Cube V → ℝ) : (finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)) = ∑ i : Fin P.count, finiteAvg fun (x : Cube V) => G x * indicator ((P.piece i).eval x)

theorem Complexity.DepthThreeLowerBound.SparsePartition.abs_correlation_le {V : Type u} [Fintype V] {H : CNF V} {b M : ℕ} {η δ : ℝ} (P : SparsePartition H b M η) (G : Cube V → ℝ) (hδ : 0 ≤ δ) (hpiece : ∀ (i : Fin P.count), |finiteAvg fun (x : Cube V) => G x * indicator ((P.piece i).eval x)| ≤ δ) : |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ 2 ^ (η * ↑(Fintype.card V)) * δ

theorem Complexity.DepthThreeLowerBound.exists_sparse_correlation_transfer (b : ℕ) (η : ℝ) (hb : 1 ≤ b) (hη : 0 < η) : ∃ (M : ℕ), 0 < M ∧ ∀ (V : Type u) [inst : Fintype V] [inst_1 : DecidableEq V] (G : Cube V → ℝ) (δ : ℝ), 0 ≤ δ → (∀ (H : CNF V), H.Normalized → H.WidthAtMost b → List.length H ≤ M * Fintype.card V → |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ δ) → corr b G ≤ 2 ^ (η * ↑(Fintype.card V)) * δ

theorem Complexity.DepthThreeLowerBound.exists_sparse_correlation_constant (b : ℕ) (hb : 1 ≤ b) : ∃ (M : ℕ), 0 < M ∧ ∀ (V : Type u) [inst : Fintype V] [inst_1 : DecidableEq V] (G : Cube V → ℝ), (∀ (H : CNF V), H.Normalized → H.WidthAtMost b → List.length H ≤ M * Fintype.card V → |finiteAvg fun (x : Cube V) => G x * indicator (H.eval x)| ≤ 2 ^ (-↑(Fintype.card V) / 4)) → corr b G ≤ 2 ^ (-↑(Fintype.card V) / 8)