Unrestricted depth-three lower bound: restriction expected cost

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

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

theorem Complexity.DepthThreeLowerBound.pathCoveredCount_eq_of_support {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (x : Cube (Live σ)) (hn : ∀ i ∈ P, (C i).Normalized) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (h : Fin P.length) : pathCoveredCount C σ P h = coveredCount (fun (i : I) => (C i).scope) (liveSet σ) (fun (i : I) => (C i).violation (fill σ x)) (pathPrefixSet C σ P h)

theorem Complexity.DepthThreeLowerBound.pathWeight_eq_coveredPathWeight_of_support {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (x : Cube (Live σ)) (hn : ∀ i ∈ P, (C i).Normalized) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) : pathWeight C σ P = coveredPathWeight (fun (i : I) => (C i).scope) (liveSet σ) (fun (i : I) => (C i).violation (fill σ x)) P

theorem Complexity.DepthThreeLowerBound.pathWeight_eq_finiteAvg_supported {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) : (if pathCompatible C σ P then pathWeight C σ P else 0) = finiteAvg fun (x : Cube (Live σ)) => if ∀ i ∈ P, (C i).violation (fill σ x) = true then 2 ^ (pathFinalSet C σ P).card * coveredPathWeight (fun (i : I) => (C i).scope) (liveSet σ) (fun (i : I) => (C i).violation (fill σ x)) P else 0

noncomputable def Complexity.DepthThreeLowerBound.fullAssignmentPathCost {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (j : ℕ) (y : Cube V) : ℝ

Evaluate the path-expansion cost on a full assignment.

Equations

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

theorem Complexity.DepthThreeLowerBound.pathCost_eq_finiteAvg_supported {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (j : ℕ) (hn : ∀ (i : I), (C i).Normalized) : pathCost C b σ j = finiteAvg fun (x : Cube (Live σ)) => fullAssignmentPathCost C b σ j (fill σ x)

theorem Complexity.DepthThreeLowerBound.restrictionAvg_pathCost_reweight {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (p : ℝ) (b j : ℕ) (hn : ∀ (i : I), (C i).Normalized) : (restrictionAvg p fun (σ : Restriction V) => pathCost C b σ j) = finiteAvg fun (y : Cube V) => ∑ T : Finset V, bernoulliWeight p T * fullAssignmentPathCost C b (maskRestriction T y) j y

theorem Complexity.DepthThreeLowerBound.restrictionAvg_pathCost_le {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (b k j : ℕ) (hn : ∀ (i : I), (C i).Normalized) (hwidth : ∀ (i : I), (C i).scope.card ≤ k) : (restrictionAvg p fun (σ : Restriction V) => pathCost C b σ j) ≤ reverseTheta (2 * p / (1 - p)) b k ^ j

theorem Complexity.DepthThreeLowerBound.restrictionAvg_restrictionCost_le_sum {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (b k : ℕ) (hn : ∀ (i : I), (C i).Normalized) (hwidth : ∀ (i : I), (C i).scope.card ≤ k) : (restrictionAvg p fun (σ : Restriction V) => restrictionCost C b σ) ≤ ∑ j ∈ Finset.range (Fintype.card V / (b + 1) + 1), reverseTheta (2 * p / (1 - p)) b k ^ j

theorem Complexity.DepthThreeLowerBound.restrictionAvg_restrictionCost_le {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (b k : ℕ) (hn : ∀ (i : I), (C i).Normalized) (hwidth : ∀ (i : I), (C i).scope.card ≤ k) (hθ : reverseTheta (2 * p / (1 - p)) b k < 1) : (restrictionAvg p fun (σ : Restriction V) => restrictionCost C b σ) ≤ (1 - reverseTheta (2 * p / (1 - p)) b k)⁻¹