Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.LanguageParameterBounds

Unrestricted depth-three lower bound: language parameter bounds #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageParameterBounds.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.hashDimension_rpow_lower (d : ℕ) :
↑d ^ (2 / 3) ≤ ↑(hashDimension d)
source
theorem Complexity.DepthThreeLowerBound.hashDimension_rpow_lt_add_one (d : ℕ) (hd : 0 < d) :
↑(hashDimension d) < ↑d ^ (2 / 3) + 1
source
theorem Complexity.DepthThreeLowerBound.hashDimension_rpow_upper (d : ℕ) (hd : 1 ≤ d) :
↑(hashDimension d) ≤ 2 * ↑d ^ (2 / 3)
source
theorem Complexity.DepthThreeLowerBound.independenceOrder_rpow_le (d : ℕ) :
↑(independenceOrder d) ≤ ↑d ^ (1 / 6)
source
theorem Complexity.DepthThreeLowerBound.rpow_lt_independenceOrder_add_two (d : ℕ) :
↑d ^ (1 / 6) < ↑(independenceOrder d) + 2
source
theorem Complexity.DepthThreeLowerBound.four_le_rpow_one_sixth (d : ℕ) (hd : 4096 ≤ d) :
4 ≤ ↑d ^ (1 / 6)
source
theorem Complexity.DepthThreeLowerBound.half_rpow_le_independenceOrder (d : ℕ) (hd : 4096 ≤ d) :
↑d ^ (1 / 6) / 2 ≤ ↑(independenceOrder d)
source
theorem Complexity.DepthThreeLowerBound.independenceOrder_add_two_mul_hashDimension_le (d : ℕ) (hd : 4096 ≤ d) :
(independenceOrder d + 2) * hashDimension d ≤ 3 * d
source
theorem Complexity.DepthThreeLowerBound.blockLen_le_five_mul (d : ℕ) (hd : 4096 ≤ d) :
blockLen d ≤ 5 * d
source
theorem Complexity.DepthThreeLowerBound.blockLen_dataDimension_le (n : ℕ) (hn : 20480 ≤ n) :
blockLen (dataDimension n) ≤ n