Unrestricted depth-three lower bound: restriction

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

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

noncomputable def Complexity.DepthThreeLowerBound.restrictionTheta (k b : ℕ) (p : ℝ) : ℝ

The parameter controlling the random-restriction expansion.

Equations

• Complexity.DepthThreeLowerBound.restrictionTheta k b p = ∑ l ∈ Finset.Icc (b + 1) k, ↑(k.choose l) * (2 * p / (1 - p)) ^ l

theorem Complexity.DepthThreeLowerBound.restrictionTheta_eq_reverseTheta (k b : ℕ) (p : ℝ) : restrictionTheta k b p = reverseTheta (2 * p / (1 - p)) b k

noncomputable def Complexity.DepthThreeLowerBound.cnfRestrictionCost {V : Type uDepth1} [Fintype V] (H : CNF V) (b : ℕ) (σ : Restriction V) : ℝ

The restriction-expansion cost associated with a CNF.

Equations

• Complexity.DepthThreeLowerBound.cnfRestrictionCost H b σ = Complexity.DepthThreeLowerBound.restrictionCost (Complexity.DepthThreeLowerBound.cnfIndexFamily H.normalize) b σ

theorem Complexity.DepthThreeLowerBound.cnfRestrictionCost_nonneg {V : Type uDepth1} [Fintype V] (H : CNF V) (b : ℕ) (σ : Restriction V) : 0 ≤ cnfRestrictionCost H b σ

theorem Complexity.DepthThreeLowerBound.cnf_restricted_correlation_le_cost {V : Type uDepth1} [Fintype V] (H : CNF V) (b : ℕ) (hb : 1 ≤ b) (σ : Restriction V) (G : Cube (Live σ) → ℝ) : |finiteAvg fun (x : Cube (Live σ)) => G x * indicator (H.eval (fill σ x))| ≤ cnfRestrictionCost H b σ * corr b G

theorem Complexity.DepthThreeLowerBound.restrictionAvg_cnfRestrictionCost_le {V : Type uDepth1} [Fintype V] (H : CNF V) (b k : ℕ) (hH : H.WidthAtMost k) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (hθ : restrictionTheta k b p < 1) : restrictionAvg p (cnfRestrictionCost H b) ≤ 1 / (1 - restrictionTheta k b p)

theorem Complexity.DepthThreeLowerBound.cnf_restriction_bound {V : Type uDepth1} [Fintype V] (H : CNF V) (b k : ℕ) (hb : 1 ≤ b) (hH : H.WidthAtMost k) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (hθ : restrictionTheta k b p < 1) : ∃ (W : Restriction V → ℝ), (∀ (σ : Restriction V), 0 ≤ W σ) ∧ restrictionAvg p W ≤ 1 / (1 - restrictionTheta k b p) ∧ ∀ (σ : Restriction V) (G : Cube (Live σ) → ℝ), |finiteAvg fun (x : Cube (Live σ)) => G x * indicator (H.eval (fill σ x))| ≤ W σ * corr b G

theorem Complexity.DepthThreeLowerBound.restrictionAvg_cnfRestrictionCost_le_two {V : Type uDepth1} [Fintype V] (H : CNF V) (b k : ℕ) (hH : H.WidthAtMost k) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (hθ : restrictionTheta k b p ≤ 1 / 2) : restrictionAvg p (cnfRestrictionCost H b) ≤ 2