Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.AlgebraPolynomial

Unrestricted depth-three lower bound: algebra polynomial #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/AlgebraPolynomial.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.BinaryAlgebra.pack {r : ℕ} (v : Fin r → ZMod 2) :
Polynomial (ZMod 2)

Pack a finite vector of field elements as polynomial coefficients.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degree_pack_lt {r : ℕ} (v : Fin r → ZMod 2) :
    (pack v).degree < ↑r
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coeff_pack {r : ℕ} (v : Fin r → ZMod 2) (i : Fin r) :
    (pack v).coeff ↑i = v i
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coeff_pack_of_le {r : ℕ} (v : Fin r → ZMod 2) {j : ℕ} (hj : r ≤ j) :
    (pack v).coeff j = 0
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coeff_pack_nat {r : ℕ} (v : Fin r → ZMod 2) (j : ℕ) :
    (pack v).coeff j = if h : j < r then v ⟨j, h⟩ else 0
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_injective {r : ℕ} :
    Function.Injective pack
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_zero {r : ℕ} :
    pack 0 = 0
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_add {r : ℕ} (v w : Fin r → ZMod 2) :
    pack (v + w) = pack v + pack w
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_smul {r : ℕ} (c : ZMod 2) (v : Fin r → ZMod 2) :
    pack (c • v) = c • pack v
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_coeff_of_degree_lt {r : ℕ} (f : Polynomial (ZMod 2)) (hf : f.degree < ↑r) :
    (pack fun (i : Fin r) => f.coeff ↑i) = f
    source
    noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial {r : ℕ} (v : Fin r → ZMod 2) :
    Polynomial (ZMod 2)

    The monic polynomial obtained from its lower coefficients.

    Equations
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_monic {r : ℕ} (v : Fin r → ZMod 2) :
      (inputPolynomial v).Monic
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_degree {r : ℕ} (v : Fin r → ZMod 2) :
      (inputPolynomial v).degree = ↑r
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_natDegree {r : ℕ} (v : Fin r → ZMod 2) :
      (inputPolynomial v).natDegree = r
      source
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_ne_zero {r : ℕ} (v : Fin r → ZMod 2) :
      inputPolynomial v ≠ 0
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_coeff_lt {r : ℕ} (v : Fin r → ZMod 2) (i : Fin r) :
      (inputPolynomial v).coeff ↑i = v i
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_coeff_leading {r : ℕ} (v : Fin r → ZMod 2) :
      (inputPolynomial v).coeff r = 1
      source
      theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomial_coeff_of_gt {r : ℕ} (v : Fin r → ZMod 2) {j : ℕ} (hj : r < j) :
      (inputPolynomial v).coeff j = 0
      source
      noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits {r : ℕ} (p : Fin r → Bool) :
      Polynomial (ZMod 2)

      The monic input polynomial specified by Boolean coefficient bits.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_monic {r : ℕ} (p : Fin r → Bool) :
        (inputPolynomialBits p).Monic
        source
        @[simp]
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_degree {r : ℕ} (p : Fin r → Bool) :
        (inputPolynomialBits p).degree = ↑r
        source
        @[simp]
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_natDegree {r : ℕ} (p : Fin r → Bool) :
        (inputPolynomialBits p).natDegree = r
        source
        @[simp]
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_coeff_lt {r : ℕ} (p : Fin r → Bool) (i : Fin r) :
        (inputPolynomialBits p).coeff ↑i = bitValue (p i)
        source
        @[simp]
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_coeff_leading {r : ℕ} (p : Fin r → Bool) :
        (inputPolynomialBits p).coeff r = 1