Change of parameter for ordinary Wronskians #
If two derivations on a field satisfy D = a • E, then the i-th iterate of
D is a^i times the i-th iterate of E, up to lower-order iterates of
E. Thus the corresponding Wronskian matrices differ by a lower-triangular
matrix whose diagonal is 1, a, a^2, .... This file records that argument;
in particular it does not make the false simplification (a • E)^i = a^i • E^i.
theorem
BGS.CorvajaZannier.derivationWronskian_det_changeParameter
{C : Type u_1}
{L : Type u_2}
[Field C]
[Field L]
[Algebra C L]
(D E : Derivation C L L)
(a : L)
(hD : D = a • E)
{n : ℕ}
(f : Fin n → L)
:
Change-of-parameter formula for an ordinary Wronskian.
The triangular exponent is n.choose 2 = 0 + 1 + ... + (n - 1). The proof
keeps all lower-order terms arising from differentiating a; they form the
strictly lower-triangular part of changeParameterMatrix and hence do not
affect its determinant.