Unrestricted depth-three lower bound: circuit deletion

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

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

theorem Complexity.DepthThreeLowerBound.Clause.violation_probability {V : Type uDepth1} [Fintype V] (C : Clause V) (hC : C.Normalized) : (finiteAvg fun (x : Cube V) => indicator (C.violation x)) = (2 ^ C.width)⁻¹

theorem Complexity.DepthThreeLowerBound.Clause.false_probability {V : Type uDepth1} [Fintype V] (C : Clause V) (hC : C.Normalized) : (finiteAvg fun (x : Cube V) => 1 - indicator (C.eval x)) = (2 ^ C.width)⁻¹

noncomputable def Complexity.DepthThreeLowerBound.CNF.deleteWide {V : Type uDepth1} (H : CNF V) (k : ℕ) : CNF V

Discard clauses whose width exceeds the given cutoff.

Equations

• H.deleteWide k = List.filter (fun (C : Complexity.DepthThreeLowerBound.Clause V) => decide (C.width ≤ k)) H

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.mem_deleteWide {V : Type uDepth1} {H : CNF V} {k : ℕ} {C : Clause V} : C ∈ H.deleteWide k ↔ C ∈ H ∧ C.width ≤ k

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.deleteWide_nil {V : Type uDepth1} (k : ℕ) : deleteWide [] k = []

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.deleteWide_cons {V : Type uDepth1} (C : Clause V) (H : CNF V) (k : ℕ) : deleteWide (C :: H) k = if C.width ≤ k then C :: H.deleteWide k else H.deleteWide k

theorem Complexity.DepthThreeLowerBound.CNF.deleteWide_widthAtMost {V : Type uDepth1} (H : CNF V) (k : ℕ) : (H.deleteWide k).WidthAtMost k

theorem Complexity.DepthThreeLowerBound.CNF.deleteWide_normalized {V : Type uDepth1} (H : CNF V) (hH : H.Normalized) (k : ℕ) : (H.deleteWide k).Normalized

theorem Complexity.DepthThreeLowerBound.CNF.deleteWide_length_le {V : Type uDepth1} (H : CNF V) (k : ℕ) : List.length (H.deleteWide k) ≤ List.length H

theorem Complexity.DepthThreeLowerBound.CNF.eval_deleteWide_of_eval {V : Type uDepth1} (H : CNF V) (k : ℕ) {x : Cube V} (hx : H.eval x = true) : (H.deleteWide k).eval x = true

theorem Complexity.DepthThreeLowerBound.CNF.indicator_eval_le_deleteWide {V : Type uDepth1} (H : CNF V) (k : ℕ) (x : Cube V) : indicator (H.eval x) ≤ indicator ((H.deleteWide k).eval x)

theorem Complexity.DepthThreeLowerBound.CNF.deletion_error_cons_le {V : Type uDepth1} (C : Clause V) (H : CNF V) (k : ℕ) (x : Cube V) : indicator ((deleteWide (C :: H) k).eval x) - indicator (eval (C :: H) x) ≤ indicator ((H.deleteWide k).eval x) - indicator (H.eval x) + if C.width ≤ k then 0 else 1 - indicator (C.eval x)

theorem Complexity.DepthThreeLowerBound.CNF.deletion_error_bound {V : Type uDepth1} [Fintype V] (H : CNF V) (hH : H.Normalized) (k : ℕ) : (finiteAvg fun (x : Cube V) => indicator ((H.deleteWide k).eval x) - indicator (H.eval x)) ≤ ↑(List.length H) * (2 ^ k)⁻¹