Integer coefficient matrices for the closed-form irreducibility criterion. Columns encode pairs of polynomials in a finite rectangular monomial grid. Rows are coefficient positions; finite independent rows will be selected when extracting a determinant witness.

@[reducible, inline]

abbrev CCDN.BivariateGrid (d : ℕ) : Type

Index set of the bivariate monomials whose outer and inner exponents are both less than d.

Equations

• CCDN.BivariateGrid d = (Fin d × Fin d)

@[reducible, inline]

abbrev CCDN.ClosedFormColumns (d : ℕ) : Type

Index set of the unknown coefficients of a pair of polynomials supported in the grid BivariateGrid d; these index the columns of the closed-form coefficient matrix.

Equations

• CCDN.ClosedFormColumns d = (CCDN.BivariateGrid d ⊕ CCDN.BivariateGrid d)

noncomputable def CCDN.bivariateGridPolynomial (R : Type u_1) [CommRing R] (d : ℕ) : (BivariateGrid d → R) →ₗ[R] Polynomial (Polynomial R)

Reconstruct a polynomial with outer and inner exponents less than d.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.bivariateGridPolynomial_coeff {R : Type u_1} [CommRing R] {d : ℕ} (v : BivariateGrid d → R) (i j : Fin d) : (((bivariateGridPolynomial R d) v).coeff ↑i).coeff ↑j = v (i, j)

The coefficient with outer exponent i and inner exponent j of the polynomial with grid coefficients v is v (i, j).

theorem CCDN.bivariateGridPolynomial_degree_lt {R : Type u_1} [CommRing R] {d : ℕ} (v : BivariateGrid d → R) : ((bivariateGridPolynomial R d) v).degree < ↑d

The polynomial with coefficients v on the grid BivariateGrid d has outer degree less than d.

noncomputable def CCDN.closedFormPair (R : Type u_1) [CommRing R] (d : ℕ) : (ClosedFormColumns d → R) →ₗ[R] Polynomial (Polynomial R) × Polynomial (Polynomial R)

Decode the two blocks of the unknown coefficient vector.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.closedFormPair_injective {R : Type u_1} [CommRing R] (d : ℕ) : Function.Injective ⇑(closedFormPair R d)

Decoding a coefficient vector into a pair of grid polynomials is injective.

noncomputable def CCDN.closedFormOperator {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) : Polynomial (Polynomial R) × Polynomial (Polynomial R) →ₗ[R] Polynomial (Polynomial R)

The cleared differential equation as a linear operator on (P,Q).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CCDN.bivariateCoefficients (R : Type u_1) [CommRing R] : Polynomial (Polynomial R) →ₗ[R] ℕ × ℕ → R

All polynomial coefficients as a linear map.

Equations

• CCDN.bivariateCoefficients R = { toFun := fun (f : Polynomial (Polynomial R)) (i : ℕ × ℕ) => (f.coeff i.1).coeff i.2, map_add' := ⋯, map_smul' := ⋯ }

theorem CCDN.bivariateCoefficients_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑(bivariateCoefficients R)

A bivariate polynomial is determined by its coefficients.

noncomputable def CCDN.closedFormCoefficientMatrix {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) : Matrix (ℕ × ℕ) (ClosedFormColumns d) R

The matrix of the closed-form equation on bounded unknowns. In particular it is an integer matrix when R=Z.

Equations

• CCDN.closedFormCoefficientMatrix d f = LinearMap.toMatrix' (CCDN.bivariateCoefficients R ∘ₗ CCDN.closedFormOperator f ∘ₗ CCDN.closedFormPair R d)

theorem CCDN.closedFormCoefficientMatrix_kernel {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) (v : ClosedFormColumns d → R) : (closedFormCoefficientMatrix d f).mulVec v = 0 ↔ (closedFormOperator f) ((closedFormPair R d) v) = 0

Matrix kernel membership is precisely the polynomial closed-form equation.