Universal homogeneous coefficient minors of the Euler-restricted operator. The constructed forms have degree exactly d^2-1 in the homogeneous sense, specialize to coefficient minors, and detect normalized irreducibility in characteristic zero. Reducibility vanishing and height bounds are separate.

noncomputable def CCDN.eulerCoefficientMonomial (R : Type u_1) [CommRing R] (d : ℕ) (i : EulerLowIndex d) : Polynomial (Polynomial R)

The bivariate monomial with coefficient one indexed by i, of total degree at most d.

Equations

• CCDN.eulerCoefficientMonomial R d i = (CCDN.bivariatePolynomialEquiv R) ((MvPolynomial.monomial ↑((Finsupp.degreeLeEquivSym (Fin 2) d).symm i)) 1)

noncomputable def CCDN.eulerCoefficientData {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) (i : EulerLowIndex d) : R

The coefficient of f at the bivariate monomial of total degree at most d indexed by i.

Equations

• CCDN.eulerCoefficientData d f i = ((CCDN.bivariatePolynomialEquiv R).symm f).coeff ↑((Finsupp.degreeLeEquivSym (Fin 2) d).symm i)

theorem CCDN.eulerCoefficientData_reconstruct {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) (hf : bivariateTotalDegree f ≤ d) : ∑ i : EulerLowIndex d, eulerCoefficientData d f i • eulerCoefficientMonomial R d i = f

A bivariate polynomial of total degree at most d is the sum of the monomials eulerCoefficientMonomial R d i weighted by its coefficients eulerCoefficientData d f i.

theorem CCDN.eulerCoefficientMonomial_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (d : ℕ) (i : EulerLowIndex d) : (bivariateMap φ) (eulerCoefficientMonomial R d i) = eulerCoefficientMonomial S d i

Applying a coefficient ring homomorphism fixes the monomials eulerCoefficientMonomial.

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

The differential operator is linear in the defining equation as well as in its pair of unknowns.

Equations

• CCDN.closedFormEquationLinear u = { toFun := fun (f : Polynomial (Polynomial R)) => (CCDN.closedFormOperator f) u, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def CCDN.eulerCoefficientEntryLinear {R : Type u_1} [CommRing R] (k : ℕ) (row : ℕ × ℕ) (col : EulerColumns k) : Polynomial (Polynomial R) →ₗ[R] R

The (row, col) entry of the Euler closed-form coefficient matrix, as a linear function of the equation.

Equations

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

noncomputable def CCDN.universalEulerMatrix (k : ℕ) : Matrix (ℕ × ℕ) (EulerColumns k) (MvPolynomial (EulerLowIndex (k + 2)) ℤ)

Integer universal matrix in all coefficients of a degree-at-most-d equation.

Equations

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

theorem CCDN.universalEulerMatrix_specialize {R : Type u_1} [CommRing R] (k : ℕ) (f : Polynomial (Polynomial R)) (hf : bivariateTotalDegree f ≤ k + 2) : (universalEulerMatrix k).map ⇑(MvPolynomial.eval₂Hom (Int.castRingHom R) (eulerCoefficientData (k + 2) f)) = eulerClosedFormCoefficientMatrix k f

Every universal matrix entry specializes to the differential coefficient matrix, with no characteristic restriction.