Point-evaluated gradients and Hessians

Formal derivatives define gradients and Hessians over any commutative semiring. The product rule expresses a product's Hessian as a linear combination of the two Hessians and two outer products of gradients. No assumption on the characteristic is needed.

Main definitions

• MvPolynomial.gradient: the gradient at a point.
• MvPolynomial.hessian: the Hessian matrix at a point.

Main results

• MvPolynomial.hessian_add, MvPolynomial.hessian_C, MvPolynomial.hessian_X.
• MvPolynomial.hessian_mul: the product rule for Hessians.
• MvPolynomial.hessian_sum_X_mul_X: the pairing polynomial has a block-swap Hessian.

References

• Ported from LowerBound/Fusion/Arithmetic/Interaction/Hessian.lean and its Pairing.lean application in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

noncomputable def MvPolynomial.gradient {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (p : MvPolynomial ι R) : ι → R

The gradient of a formal polynomial, evaluated at a point.

noncomputable def MvPolynomial.hessian {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (p : MvPolynomial ι R) : Matrix ι ι R

The Hessian of a formal polynomial, evaluated at a point.

@[simp]

theorem MvPolynomial.hessian_add {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (p q : MvPolynomial ι R) : hessian x (p + q) = hessian x p + hessian x q

The Hessian of a sum is the sum of the Hessians.

@[simp]

theorem MvPolynomial.hessian_C {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (c : R) : hessian x (C c) = 0

A constant polynomial has zero Hessian.

@[simp]

theorem MvPolynomial.hessian_X {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (i : ι) : hessian x (X i) = 0

A variable has zero Hessian.

theorem MvPolynomial.hessian_mul {ι : Type u_1} {R : Type u_2} [CommSemiring R] (x : ι → R) (p q : MvPolynomial ι R) : hessian x (p * q) = (eval x) q • hessian x p + (eval x) p • hessian x q + (Matrix.vecMulVec (gradient x p) (gradient x q) + Matrix.vecMulVec (gradient x q) (gradient x p))

A product's Hessian has two additional outer products of gradients.

theorem MvPolynomial.hessian_sum_X_mul_X {ι : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] (point : ι ⊕ ι → R) : hessian point (∑ i : ι, X (Sum.inl i) * X (Sum.inr i)) = Matrix.submatrix 1 ⇑(Equiv.sumComm ι ι) ⇑(Equiv.refl (ι ⊕ ι))

The Hessian of the pairing polynomial swaps the two coordinate blocks. This identity holds over any commutative semiring, including characteristic two.