Minimum residual Hessian rank

Subtracting arbitrary linear combinations of supplied Hessians gives a family of residual matrices. Their minimum rank is recorded in ℕ∞, for comparison with extended circuit costs. Unlike circuit complexity, this minimum is always finite: zero coefficients are available. The coefficients are chosen at the given point, not uniformly over all points.

Main definitions

• MvPolynomial.hessianResidualRank: minimum rank after subtracting supplied Hessians.

Main results

• MvPolynomial.hessianResidualRank_le: any choice of coefficients bounds the minimum.
• MvPolynomial.hessianResidualRank_ne_top: the minimum is finite.

References

• Ported from LowerBound/Fusion/Arithmetic/Interaction/Hessian/Relative.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

noncomputable def MvPolynomial.hessianResidualRank {ι : Type u_1} {κ : Type u_2} {K : Type u_3} [Field K] [Fintype ι] [Fintype κ] (point : ι → K) (target : MvPolynomial ι K) (sources : κ → MvPolynomial ι K) : ℕ∞

The minimum residual Hessian rank at a fixed point after subtracting a linear combination of the supplied Hessians. The result lies in ℕ∞ to compare with extended computational costs.

theorem MvPolynomial.hessianResidualRank_le {ι : Type u_1} {κ : Type u_2} {K : Type u_3} [Field K] [Fintype ι] [Fintype κ] (point : ι → K) (target : MvPolynomial ι K) (sources : κ → MvPolynomial ι K) (coefficients : κ → K) : hessianResidualRank point target sources ≤ ↑(hessian point target - ∑ i : κ, coefficients i • hessian point (sources i)).rank

The minimum residual Hessian rank is at most the rank of the residual for any choice of coefficients.

@[simp]

theorem MvPolynomial.hessianResidualRank_ne_top {ι : Type u_1} {κ : Type u_2} {K : Type u_3} [Field K] [Fintype ι] [Fintype κ] (point : ι → K) (target : MvPolynomial ι K) (sources : κ → MvPolynomial ι K) : hessianResidualRank point target sources ≠ ⊤

The minimum residual Hessian rank is finite.