Degree-correct logarithmic factor forms for the Euler-restricted operator. The construction works in every characteristic.
noncomputable def
CCDN.eulerFactorPair
{R : Type u_1}
[CommRing R]
(a b : ℕ)
(g h : Polynomial (Polynomial R))
:
The logarithmic factor pair of g and h with weights a and b: the pair (P, Q) with
(P dx + Q dy) / (g * h) = b • dg / g - a • dh / h, so P = b • h * ∂ₓg - a • g * ∂ₓh for the
outer derivative ∂ₓ and Q = b • h * ∂ᵧg - a • g * ∂ᵧh for the inner derivative ∂ᵧ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.exists_eulerFactorKernel
{F : Type u_1}
[Field F]
(k a b : ℕ)
(ha : 0 < a)
(hb : 0 < b)
(hab : a + b = k + 2)
(g h : Polynomial (Polynomial F))
(hg : bivariateTotalDegree g ≤ a)
(hh : bivariateTotalDegree h ≤ b)
(hne : eulerFactorPair a b g h ≠ 0)
:
∃ (u : EulerPairSpace F k), u ≠ 0 ∧ (eulerClosedFormOperator k (g * h)) u = 0
If g and h have total degrees at most a and b with a, b > 0 and a + b = k + 2, and
their logarithmic factor pair is nonzero, then the Euler closed-form operator of g * h has a
nonzero kernel vector in EulerPairSpace F k.