Parameter degrees of the closed-form matrix and its minors. Differentiation in the two plane coordinates does not increase the parameter degree.
def
CCDN.BivariateParameterDegreeBound
{K : Type u_1}
{τ : Type u_2}
[CommRing K]
(f : Polynomial (Polynomial (MvPolynomial τ K)))
(D : ℕ)
:
Every coefficient of the bivariate polynomial f, whose coefficients are polynomials in the
parameters τ, has total degree at most D in the parameters; the two polynomial variables are
the coordinates on the plane.
Equations
- CCDN.BivariateParameterDegreeBound f D = ∀ (i j : ℕ), ((f.coeff i).coeff j).totalDegree ≤ D
Instances For
theorem
CCDN.matrix_det_parameterDegree
{K : Type u_1}
{τ : Type u_2}
{ι : Type u_3}
[CommRing K]
[Fintype ι]
[DecidableEq ι]
(M : Matrix ι ι (MvPolynomial τ K))
(D : ℕ)
(hM : ∀ (i j : ι), (M i j).totalDegree ≤ D)
:
If every entry of a square matrix of multivariate polynomials has total degree at most D, then
its determinant has total degree at most the size of the matrix times D.
theorem
CCDN.closedForm_minor_parameterDegree
{K : Type u_1}
{τ : Type u_2}
[CommRing K]
(d r : ℕ)
(f : Polynomial (Polynomial (MvPolynomial τ K)))
(D : ℕ)
(hf : BivariateParameterDegreeBound f D)
(a : Fin r → ℕ × ℕ)
(c : Fin r → ClosedFormColumns d)
:
The parameter degree of any r-row minor is at most r times the coefficient parameter degree; no dependence on the chosen row exponents is introduced.