Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.InterpolationQuotient

Unrestricted depth-three lower bound: interpolation quotient #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/InterpolationQuotient.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.Interpolation.coefficientEncoding {r : ℕ} (p : Fin r → BinaryAlgebra.F2) (t : ℕ) :
(Fin t → Fin r → Bool) ≃ (Fin t → BinaryAlgebra.InputQuotient p)

Encode coefficient vectors in the polynomial quotient ring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.Interpolation.coefficientEncoding_apply {r t : ℕ} (p : Fin r → BinaryAlgebra.F2) (β : Fin t → Fin r → Bool) (j : Fin t) :
    (coefficientEncoding p t) β j = BinaryAlgebra.encode p fun (i : Fin r) => BinaryAlgebra.bitValue (β j i)
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_coefficientEncoding {r t : ℕ} (p : Fin r → BinaryAlgebra.F2) (Φ : (Fin t → BinaryAlgebra.InputQuotient p) → ℝ) :
    (finiteAvg fun (β : Fin t → Fin r → Bool) => Φ fun (j : Fin t) => BinaryAlgebra.encode p fun (i : Fin r) => BinaryAlgebra.bitValue (β j i)) = finiteAvg Φ
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_degreeZero {r : ℕ} (p : Fin r → BinaryAlgebra.F2) (hr : 0 < r) (Φ : BinaryAlgebra.F2 → ℝ) :
    (finiteAvg fun (z : BinaryAlgebra.InputQuotient p) => Φ ((BinaryAlgebra.degreeZero ⋯) z)) = finiteAvg Φ
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_quotient_acceptEval {r t : ℕ} (p : Fin r → BinaryAlgebra.F2) [Fact (Irreducible (BinaryAlgebra.inputPolynomial p))] (hr : 0 < r) {ι : Type uDepth1} [Fintype ι] [DecidableEq ι] (a : ι → BinaryAlgebra.InputQuotient p) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → Bool) → ℝ) :
    (finiteAvg fun (β : Fin t → BinaryAlgebra.InputQuotient p) => Φ (acceptEval (BinaryAlgebra.degreeZero ⋯) t a β)) = finiteAvg Φ
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_encoded_acceptEval {r t : ℕ} (p : Fin r → BinaryAlgebra.F2) [Fact (Irreducible (BinaryAlgebra.inputPolynomial p))] (hr : 0 < r) {ι : Type uDepth1} [Fintype ι] [DecidableEq ι] (a : ι → BinaryAlgebra.InputQuotient p) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → Bool) → ℝ) :
    (finiteAvg fun (β : Fin t → Fin r → Bool) => Φ (acceptEval (BinaryAlgebra.degreeZero ⋯) t a fun (j : Fin t) => BinaryAlgebra.encode p fun (i : Fin r) => BinaryAlgebra.bitValue (β j i))) = finiteAvg Φ
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_encoded_acceptEval_finset {r t : ℕ} (p : Fin r → BinaryAlgebra.F2) [Fact (Irreducible (BinaryAlgebra.inputPolynomial p))] (hr : 0 < r) {Z : Type uDepth2} [DecidableEq Z] (a : Z → BinaryAlgebra.InputQuotient p) (s : Finset Z) (hsize : s.card ≤ t) (ha : Set.InjOn a ↑s) (Φ : (↥s → Bool) → ℝ) :
    (finiteAvg fun (β : Fin t → Fin r → Bool) => Φ fun (z : ↥s) => acceptEval (BinaryAlgebra.degreeZero ⋯) t a (fun (j : Fin t) => BinaryAlgebra.encode p fun (i : Fin r) => BinaryAlgebra.bitValue (β j i)) ↑z) = finiteAvg Φ