Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.HardSliceSelection

Unrestricted depth-three lower bound: hard slice selection #

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

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

source
theorem Complexity.DepthThreeLowerBound.exists_small_restriction_failure {V : Type uDepth1} {Ω : Type uDepth2} [Fintype V] [Fintype Ω] [Nonempty Ω] {p δ η : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (hδ : 0 ≤ δ) (window : Restriction V → Prop) (good : Ω → Restriction V → Prop) (hfixed : ∀ (σ : Restriction V), window σ → (finiteProb fun (ω : Ω) => ¬good ω σ) ≤ δ) (hwindow : (restrictionAvg p fun (σ : Restriction V) => if ¬window σ then 1 else 0) ≤ η) :
∃ (ω : Ω), (restrictionAvg p fun (σ : Restriction V) => if ¬(window σ ∧ good ω σ) then 1 else 0) ≤ η + δ
source
def Complexity.DepthThreeLowerBound.restrictionWindow {V : Type uDepth1} [Fintype V] (p : ℝ) (σ : Restriction V) :
Prop

The allowed interval for the number of surviving coordinates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.DepthThreeLowerBound.goodRestriction {V : Type uDepth1} [Fintype V] (p ε : ℝ) (b : ℕ) (f : Cube V → Bool) (σ : Restriction V) :
    Prop

    A restriction satisfying the survival and correlation requirements.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.goodRestriction_corr {V : Type uDepth1} [Fintype V] {p ε : ℝ} {b : ℕ} {f : Cube V → Bool} {σ : Restriction V} (h : goodRestriction p ε b f σ) :
      (corr b fun (z : Cube (Live σ)) => sign (f (fill σ z))) ≤ ε
      source
      theorem Complexity.DepthThreeLowerBound.exists_good_parameter {V : Type uDepth1} {Ω : Type uDepth2} [Fintype V] [instDecidableEqV : DecidableEq V] [Fintype Ω] [Nonempty Ω] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (b : ℕ) (f : Ω → Cube V → Bool) (hfixed : ∀ (σ : Restriction V), restrictionWindow p σ → (finiteProb fun (ω : Ω) => ¬(corr b fun (z : Cube (Live σ)) => sign (f ω (fill σ z))) ≤ 2 ^ (-(p * ↑(Fintype.card V)) / 16)) ≤ 2 * 2 ^ (-(p * ↑(Fintype.card V)) / 16)) :
      ∃ (ω : Ω), (restrictionAvg p fun (σ : Restriction V) => if ¬goodRestriction p (2 ^ (-(p * ↑(Fintype.card V)) / 16)) b (f ω) σ then 1 else 0) ≤ 4 * 2 ^ (-(p * ↑(Fintype.card V)) / 16)