Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Progress.Separated.Polynomial

Coefficient-one polynomials from finite monomial families #

This module turns any finite family of exponent vectors into the polynomial having exactly those monomials, each with coefficient one. It is the reusable bridge from finite separated-family arguments to arithmetic circuit lower bounds; concrete families need only prove their finite support is separated.

source
noncomputable def Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.ofSupport {Variable : Type u_1} (support : Finset (Variable →₀ ℕ)) :
MvPolynomial Variable ℕ

The natural-coefficient polynomial with exactly the given exponent vectors, each occurring with coefficient one.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.support_ofSupport {Variable : Type u_1} (support : Finset (Variable →₀ ℕ)) :
    (ofSupport support).support = support

    ofSupport has exactly its specified monomial support.

    source
    @[simp]
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.coeff_ofSupport {Variable : Type u_1} [DecidableEq Variable] (support : Finset (Variable →₀ ℕ)) (exponent : Variable →₀ ℕ) :
    (ofSupport support).coeff exponent = if exponent ∈ support then 1 else 0

    Coefficients of ofSupport are the characteristic function of the specified support.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.coeff_ofSupport_of_mem {Variable : Type u_1} [DecidableEq Variable] {support : Finset (Variable →₀ ℕ)} {exponent : Variable →₀ ℕ} (present : exponent ∈ support) :
    (ofSupport support).coeff exponent = 1

    Every specified monomial has coefficient one.

    source
    theorem Algebraic.Fusion.Arithmetic.Progress.Separated.Polynomial.circuit_addition_lowerBound {n : ℕ} (support : Finset (Fin n →₀ ℕ)) (separated : IsSeparated support support) (circuit : Circuit (Arithmetic.signature PEmpty.{u_1 + 1}) n 1) (constructs : { inputCount := n, inputs := MvPolynomial.X, target := ofSupport support }.Constructs circuit (polynomialInterpretation (Fin n))) :
    support.card - 1 ≤ circuit.cost Arithmetic.additionCost

    A separated finite family yields its cardinality-minus-one addition lower bound for every constant-free monotone arithmetic circuit computing its coefficient-one polynomial.