Unrestricted depth-three lower bound: restriction cost correlation

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

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

theorem Complexity.DepthThreeLowerBound.pathMixture_eq_pathTerm {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) {n : ℕ} {P : List I} (hP : P ∈ paths (fun (i : I) => (C i).scope) (liveSet σ) b n) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (K : CNF (Live σ)) (x : Cube (Live σ)) : (pathWeight C σ P * finiteAvg fun (π : PathMarkerSample C b σ P) => indicator ((pathMixtureCNF C b σ P K π).eval x)) = indicator (K.eval x) * pathTerm (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) P

theorem Complexity.DepthThreeLowerBound.pathTerm_zero_of_incompatible {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (hc : ¬pathCompatible C σ P) (x : Cube (Live σ)) : pathTerm (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) P = 0

theorem Complexity.DepthThreeLowerBound.abs_corr_pathTerm_le {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) {n : ℕ} {P : List I} (hP : P ∈ paths (fun (i : I) => (C i).scope) (liveSet σ) b n) (hn : ∀ i ∈ P, (C i).Normalized) (hb : 1 ≤ b) (K : CNF (Live σ)) (hK : K.WidthAtMost b) (G : Cube (Live σ) → ℝ) : |finiteAvg fun (x : Cube (Live σ)) => G x * (indicator (K.eval x) * pathTerm (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) P)| ≤ (if pathCompatible C σ P then pathWeight C σ P else 0) * corr b G

noncomputable def Complexity.DepthThreeLowerBound.pathLayer {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (K : CNF (Live σ)) (n : ℕ) (x : Cube (Live σ)) : ℝ

The contribution of paths of a specified length to the restriction expansion.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DepthThreeLowerBound.abs_corr_pathLayer_le {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (hn : ∀ (i : I), (C i).Normalized) (b : ℕ) (hb : 1 ≤ b) (σ : Restriction V) (K : CNF (Live σ)) (hK : K.WidthAtMost b) (n : ℕ) (G : Cube (Live σ) → ℝ) : |finiteAvg fun (x : Cube (Live σ)) => G x * pathLayer C b σ K n x| ≤ pathCost C b σ n * corr b G

theorem Complexity.DepthThreeLowerBound.indexedCNF_restriction_expansion {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (x : Cube (Live σ)) : indicator ((indexedCNF C).eval (fill σ x)) = indicator ((easyBaseCNF C b σ).eval x) + ∑ j ∈ Finset.range ((liveSet σ).card / (b + 1)), (-1) ^ (j + 1) * pathLayer C b σ (easyBaseCNF C b σ) (j + 1) x

theorem Complexity.DepthThreeLowerBound.initial_and_live_path_cost_le {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : 1 + ∑ j ∈ Finset.range ((liveSet σ).card / (b + 1)), pathCost C b σ (j + 1) ≤ restrictionCost C b σ

theorem Complexity.DepthThreeLowerBound.restricted_correlation_le_cost {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (hb : 1 ≤ b) (hn : ∀ (i : I), (C i).Normalized) (σ : Restriction V) (G : Cube (Live σ) → ℝ) : |finiteAvg fun (x : Cube (Live σ)) => G x * indicator ((indexedCNF C).eval (fill σ x))| ≤ restrictionCost C b σ * corr b G