Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.FinalParameterBounds

Unrestricted depth-three lower bound: final parameter bounds #

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

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

source
noncomputable def Complexity.DepthThreeLowerBound.liveProbability (B : ℝ) (d : ℕ) :
ℝ

The live-coordinate probability used by the final restriction parameters.

Equations
Instances For
    source
    noncomputable def Complexity.DepthThreeLowerBound.degreeCutoff (s : ℝ) (d : ℕ) :
    ℕ

    The clause-width cutoff used in the final hard-slice bound.

    Equations
    Instances For
      source
      def Complexity.DepthThreeLowerBound.factorialBase (B s : ℝ) :
      ℝ

      The auxiliary scale used to bound the factorial contribution.

      Equations
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.liveProbability_pos (B : ℝ) (hB : 0 < B) (d : ℕ) (hd : 0 < d) :
        0 < liveProbability B d
        source
        theorem Complexity.DepthThreeLowerBound.liveProbability_mul_dimension (B : ℝ) (d : ℕ) (hd : 0 < d) :
        liveProbability B d * ↑d = B * √↑d
        source
        theorem Complexity.DepthThreeLowerBound.degreeCutoff_lower (s : ℝ) (d : ℕ) :
        3 * (s + 1) * √↑d ≤ ↑(degreeCutoff s d)
        source
        theorem Complexity.DepthThreeLowerBound.degreeCutoff_upper (s : ℝ) (hs : 0 ≤ s) (d : ℕ) (hd : 1 ≤ d) :
        ↑(degreeCutoff s d) ≤ (3 * (s + 1) + 1) * √↑d
        source
        theorem Complexity.DepthThreeLowerBound.exists_liveProbability_threshold (B : ℝ) (hB : 0 < B) :
        ∃ (D : ℕ), 1 ≤ D ∧ ∀ (d : ℕ), D ≤ d → 0 < liveProbability B d ∧ liveProbability B d ≤ 1 / 2
        source
        theorem Complexity.DepthThreeLowerBound.scaled_cutoff_le_factorialBase (B s : ℝ) (hB : 0 ≤ B) (hs : 0 ≤ s) (d : ℕ) (hd : 1 ≤ d) (hp : liveProbability B d ≤ 1 / 2) :
        2 * liveProbability B d / (1 - liveProbability B d) * ↑(degreeCutoff s d) ≤ factorialBase B s
        source
        theorem Complexity.DepthThreeLowerBound.reverseTheta_le_factorial_tail (α Q : ℝ) (hα : 0 ≤ α) (b k : ℕ) (hαk : α * ↑k ≤ Q) :
        reverseTheta α b k ≤ ∑ ℓ ∈ Finset.Ico (b + 1) (k + 1), Q ^ ℓ / ↑ℓ.factorial
        source
        theorem Complexity.DepthThreeLowerBound.exists_final_parameter_width (B s : ℝ) (hB : 0 < B) (hs : 0 ≤ s) :
        ∃ (b : ℕ), 1 ≤ b ∧ ∃ (D : ℕ), 1 ≤ D ∧ ∀ (d : ℕ), D ≤ d → 0 < liveProbability B d ∧ liveProbability B d ≤ 1 / 2 ∧ reverseTheta (2 * liveProbability B d / (1 - liveProbability B d)) b (degreeCutoff s d) ≤ 1 / 2