Documentation

Complexitylib.Algebraic.LowerBound.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary

Binary compilation of degree-parametric Waring sums #

Compile a degree-d rectangular Waring term to an ordinary arithmetic DAG: compute its d-variable linear form once, power it by binary recursion, and apply its scale. The exact multiplication charge per term is

d + binaryMultiplicationCount d + 1.

source
def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.linearFormExpression {K : Type} {degree : ℕ} [Zero K] (term : Term K degree) :
Arithmetic.Expression K degree

Arithmetic expression for a rectangular Waring linear form.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.scaleExpression {K : Type} (scale : K) :
    Arithmetic.Expression K 1

    Final scalar multiplication after the shared binary power.

    Equations
    Instances For
      source
      def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.additionExpression {K : Type} (degree : ℕ) :
      Arithmetic.Expression K (degree + 2)

      Source addition after the shared degree context variables.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termCircuit {K : Type} {degree : ℕ} [Zero K] [One K] (term : Term K degree) :
        Circuit (Arithmetic.signature K) degree 1

        Shared-linear-form, binary-power term gadget.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termCircuit_size {K : Type} {degree : ℕ} [Zero K] [One K] (term : Term K degree) :
          (termCircuit term).size = (linearFormExpression term).gateCount + (Arithmetic.Power.binaryCircuit degree).size + (scaleExpression term.scale).gateCount

          The gate count of termCircuit is the tree gate count of the linear form, plus the gate count of the binary power circuit, plus the tree gate count of the final scaling. Composing the stages adds no gates. Unlike the multiplication and addition charges below, the count includes the named-constant gates.

          source
          def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termMultiplicationCount (degree : ℕ) :
          ℕ

          Exact multiplication charge of one rectangular binary term gadget.

          Equations
          Instances For
            source
            def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termAdditionCount (degree : ℕ) :
            ℕ

            Exact addition charge of one rectangular binary term gadget.

            Equations
            Instances For
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.multiplicationCount_linearFormExpression {K : Type} {degree : ℕ} [Zero K] (term : Term K degree) :
              (linearFormExpression term).multiplicationCount = degree
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.additionCount_linearFormExpression {K : Type} {degree : ℕ} [Zero K] (term : Term K degree) :
              (linearFormExpression term).additionCount = degree
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termCircuit_multiplicationCost {K : Type} {degree : ℕ} [Zero K] [One K] (term : Term K degree) :
              (termCircuit term).cost Arithmetic.multiplicationCost = termMultiplicationCount degree
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termCircuit_additionCost {K : Type} {degree : ℕ} [Zero K] [One K] (term : Term K degree) :
              (termCircuit term).cost Arithmetic.additionCost = termAdditionCount degree
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.multiplicationCount_additionExpression {K : Type} (degree : ℕ) :
              (additionExpression degree).multiplicationCount = 0
              source
              @[simp]
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.additionCount_additionExpression {K : Type} (degree : ℕ) :
              (additionExpression degree).additionCount = 1
              source
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.eval_linearFormExpression {K : Type} {degree : ℕ} [CommSemiring K] (term : Term K degree) :
              Arithmetic.Expression.eval (⇑MvPolynomial.C) MvPolynomial.X (linearFormExpression term) = linearForm term

              The linear-form expression denotes the rectangular Waring linear form.

              source
              theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.eval_termCircuit {K : Type} {degree : ℕ} [CommSemiring K] (term : Term K degree) :
              (termCircuit term).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X 0 = termValue term

              The rectangular binary term gadget computes its charged degree-d power exactly.

              source
              def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.translation {K : Type} [Semiring K] (degree : ℕ) :
              ContextualTranslation (SumOfTerms.signature (Term K degree)) (Arithmetic.signature K) degree

              Contextual compilation of degree-d Waring sums using binary powers.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.pullCost_multiplicationCost {K : Type} [Semiring K] (degree : ℕ) :
                (translation degree).pullCost Arithmetic.multiplicationCost = SumOfTerms.weightedCost 0 (termMultiplicationCount degree)
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.pullCost_additionCost {K : Type} [Semiring K] (degree : ℕ) :
                (translation degree).pullCost Arithmetic.additionCost = SumOfTerms.weightedCost 1 (termAdditionCount degree)
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.compile_multiplicationCost_eq_termCost {K : Type} {m : ℕ} [Semiring K] (degree : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 m) :
                ((translation degree).compile circuit).cost Arithmetic.multiplicationCost = termMultiplicationCount degree * circuit.cost SumOfTerms.termCost
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.compile_additionCost_eq_sourceCosts {K : Type} {m : ℕ} [Semiring K] (degree : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 m) :
                ((translation degree).compile circuit).cost Arithmetic.additionCost = circuit.cost SumOfTerms.additionCost + termAdditionCount degree * circuit.cost SumOfTerms.termCost
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.termMultiplicationCount_le (degree : ℕ) (positive : 0 < degree) :
                termMultiplicationCount degree ≤ degree + 2 * degree.log2 + 1

                Per-term multiplication cost is degree plus logarithmic powering overhead.

                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.pull_polynomial {K : Type} [CommSemiring K] (degree : ℕ) :
                (translation degree).pull (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = SumOfTerms.interpretation termValue
                source
                theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Translation.Binary.compile_eval {K : Type} {m : ℕ} [CommSemiring K] (degree : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K degree)) 0 m) :
                ((translation degree).compile circuit).eval (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X = circuit.eval (SumOfTerms.interpretation termValue) fun (input : Fin 0) => input.elim0