Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.InterpolationEvaluation

Unrestricted depth-three lower bound: interpolation evaluation #

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

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

source
def Complexity.DepthThreeLowerBound.Interpolation.coeffEval {F : Type uDepth1} {ι : Type uDepth2} [CommSemiring F] (t : ℕ) (a : ι → F) :
(Fin t → F) →ₗ[F] ι → F

Evaluate a polynomial from its finite coefficient vector.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.Interpolation.coeffEval_apply {F : Type uDepth1} {ι : Type uDepth2} [CommSemiring F] (t : ℕ) (a : ι → F) (β : Fin t → F) (i : ι) :
    (coeffEval t a) β i = ∑ j : Fin t, β j * a i ^ ↑j
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.coeffEval_surjective {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Fintype ι] {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) :
    Function.Surjective ⇑(coeffEval t a)
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.card_coeffEval_fiber_mul {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (v : ι → F) :
    Fintype.card F ^ Fintype.card ι * Fintype.card { β : Fin t → F // (coeffEval t a) β = v } = Fintype.card F ^ t
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.card_coeffEval_fiber {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (v : ι → F) :
    Fintype.card { β : Fin t → F // (coeffEval t a) β = v } = Fintype.card F ^ (t - Fintype.card ι)
    source
    theorem Complexity.DepthThreeLowerBound.Interpolation.finiteAvg_coeffEval {F : Type uDepth1} {ι : Type uDepth2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {t : ℕ} (a : ι → F) (hsize : Fintype.card ι ≤ t) (ha : Function.Injective a) (Φ : (ι → F) → ℝ) :
    (finiteAvg fun (β : Fin t → F) => Φ ((coeffEval t a) β)) = finiteAvg Φ