Unrestricted depth-three lower bound: hard slice moment

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

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

theorem Complexity.DepthThreeLowerBound.finiteProb_abs_avg_gt_le {Ω : Type uDepth1} {Z : Type uDepth2} [Fintype Ω] [Nonempty Ω] [Fintype Z] [Nonempty Z] [DecidableEq Z] (h : ℕ) (hh : 0 < h) (bits : Ω → Z → Bool) (hdist : UniformBitsUpTo (2 * h) bits) (J : Z → Bool) (δ : ℝ) (hδ : 0 < δ) : (finiteProb fun (ω : Ω) => δ < |finiteAvg fun (z : Z) => sign (bits ω z) * indicator (J z)|) ≤ ↑(2 * h) ^ (2 * h) * ↑(Fintype.card Z) ^ h / (δ * ↑(Fintype.card Z)) ^ (2 * h)

noncomputable def Complexity.DepthThreeLowerBound.sparseMomentBound (m b L h : ℕ) (δ : ℝ) : ℝ

The moment estimate used to control sparse-CNF correlations.

Equations

• Complexity.DepthThreeLowerBound.sparseMomentBound m b L h δ = ↑(((2 * m + 1) ^ b + 1) ^ L) * (↑(2 * h) ^ (2 * h) * ↑(2 ^ m) ^ h / (δ * ↑(2 ^ m)) ^ (2 * h))

theorem Complexity.DepthThreeLowerBound.finiteProb_sparse_codes_gt_le {Ω : Type uDepth3} {V : Type uDepth4} [Fintype Ω] [Nonempty Ω] [Fintype V] (b L h : ℕ) (hh : 0 < h) (bits : Ω → Cube V → Bool) (hdist : UniformBitsUpTo (2 * h) bits) (δ : ℝ) (hδ : 0 < δ) : (finiteProb fun (ω : Ω) => ∃ (c : SparseTestCode V b L), δ < |finiteAvg fun (x : Cube V) => sign (bits ω x) * indicator (c.eval x)|) ≤ sparseMomentBound (Fintype.card V) b L h δ

theorem Complexity.DepthThreeLowerBound.finiteProb_sparse_cnfs_gt_le {Ω : Type uDepth5} {V : Type uDepth6} [Fintype Ω] [Nonempty Ω] [Fintype V] (b L h : ℕ) (hh : 0 < h) (bits : Ω → Cube V → Bool) (hdist : UniformBitsUpTo (2 * h) bits) (δ : ℝ) (hδ : 0 < δ) : (finiteProb fun (ω : Ω) => ∃ (H : CNF V), H.WidthAtMost b ∧ List.length H ≤ L ∧ δ < |finiteAvg fun (x : Cube V) => sign (bits ω x) * indicator (H.eval x)|) ≤ sparseMomentBound (Fintype.card V) b L h δ

theorem Complexity.DepthThreeLowerBound.acceptEval_uniformBitsUpTo {F : Type uDepth7} {Z : Type uDepth8} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [DecidableEq Z] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) (t : ℕ) (a : Z → F) (ha : Function.Injective a) : UniformBitsUpTo t (Interpolation.acceptEval ell t a)

theorem Complexity.DepthThreeLowerBound.coefficient_sparse_cnfs_gt_le {F : Type uDepth9} {V : Type uDepth10} [Field F] [Module BinaryAlgebra.F2 F] [Fintype F] [Fintype V] (ell : F →ₗ[BinaryAlgebra.F2] BinaryAlgebra.F2) (hOne : ell 1 = 1) (a : Cube V → F) (ha : Function.Injective a) (b L h : ℕ) (hh : 0 < h) (δ : ℝ) (hδ : 0 < δ) : (finiteProb fun (β : Fin (2 * h) → F) => ∃ (H : CNF V), H.WidthAtMost b ∧ List.length H ≤ L ∧ δ < |finiteAvg fun (x : Cube V) => sign (Interpolation.acceptEval ell (2 * h) a β x) * indicator (H.eval x)|) ≤ sparseMomentBound (Fintype.card V) b L h δ