Wronskians of polynomial families

The Wronskian of a finite family of polynomials, with derivative orders 0, …, h - 1, and the local order calculus behind the small-subspace expansion step of the rational hitting-list construction. Over a field of characteristic zero, a family with pairwise distinct vanishing orders at a point has a nonzero Wronskian whose order there is determined exactly. Since a change of basis only rescales the Wronskian, this bounds the total vanishing order of order-echelon bases at distinct points by the Wronskian's degree.

Main definitions

• Expansion.wronskianFamily: the Wronskian det (f_j^{(i)}) of a family f : Fin h → K[X].
• Expansion.vanishingFiltration: the members of a polynomial subspace vanishing to order at least r at a point.

Main results

• Expansion.wronskian_order_of_distinct_orders: the exact order at zero of the Wronskian of a family with distinct orders.
• Expansion.exists_echelon_basis_at: every bounded-degree subspace has a basis with distinct vanishing orders at a given point.
• Expansion.wronskian_order_bound: the total vanishing order of such bases at w distinct points is at most h * (d - 1) + w * (0 + 1 + ⋯ + (h - 1)).
• Expansion.finrank_vanishingFiltration: an order-echelon basis computes the dimension of every step of the vanishing filtration.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/Wronskian.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

noncomputable def Cslib.Circuits.Rational.Expansion.wronskianFamily {K : Type u_1} [CommRing K] {h : ℕ} (f : Fin h → Polynomial K) : Polynomial K

The Wronskian with derivative orders 0, ..., h - 1.

theorem Cslib.Circuits.Rational.Expansion.det_factor_column_orders {K : Type u_1} {ι : Type u_2} [CommRing K] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι (Polynomial K)) (d : ι → ℕ) (hd : ∀ (i j : ι), Polynomial.X ^ d j ∣ A i j) : ∃ (B : Matrix ι ι (Polynomial K)), A.det = (Polynomial.X ^ ∑ j : ι, d j) * B.det ∧ ∀ (i j : ι), (B i j).coeff 0 = (A i j).coeff (d j)

Factoring prescribed powers from the columns keeps track of the first possible coefficient of a determinant.

theorem Cslib.Circuits.Rational.Expansion.coeff_scaled_derivative_at {K : Type u_1} [CommRing K] (f : Polynomial K) (r d : ℕ) : (Polynomial.X ^ r * (⇑Polynomial.derivative)^[r] f).coeff d = ↑(d.descFactorial r) * f.coeff d

theorem Cslib.Circuits.Rational.Expansion.scaled_derivative_order {K : Type u_1} [CommRing K] (f : Polynomial K) (r : ℕ) : Polynomial.X ^ f.natTrailingDegree ∣ Polynomial.X ^ r * (⇑Polynomial.derivative)^[r] f

theorem Cslib.Circuits.Rational.Expansion.wronskian_order_of_distinct_orders {K : Type u_1} [Field K] [CharZero K] {h : ℕ} (f : Fin h → Polynomial K) (hf : ∀ (j : Fin h), f j ≠ 0) (hd : Function.Injective fun (j : Fin h) => (f j).natTrailingDegree) : wronskianFamily f ≠ 0 ∧ (wronskianFamily f).natTrailingDegree + ∑ i : Fin h, ↑i = ∑ j : Fin h, (f j).natTrailingDegree

The local order formula at zero, before translation to an arbitrary point. The sum of the row numbers is C(h,2).

theorem Cslib.Circuits.Rational.Expansion.exists_degree_echelon_family {K : Type u_1} [Field K] (d : ℕ) (V : Submodule K (Polynomial K)) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ (h : ℕ) (f : Fin h → Polynomial K), LinearIndependent K f ∧ Submodule.span K (Set.range f) = V ∧ Function.Injective fun (i : Fin h) => (f i).natDegree

Polynomial row reduction, derived rather than assumed: every bounded-degree subspace has a basis with distinct largest degrees.

noncomputable def Cslib.Circuits.Rational.Expansion.reflectLinearEquiv (K : Type u_1) [Field K] (N : ℕ) : Polynomial K ≃ₗ[K] Polynomial K

Fixed-length coefficient reversal is linear, unlike degree-dependent polynomial reversal.

theorem Cslib.Circuits.Rational.Expansion.order_reflect {K : Type u_1} [Field K] (N : ℕ) (f : Polynomial K) (hf : f ≠ 0) (hd : f.natDegree ≤ N) : (Polynomial.reflect N f).natTrailingDegree = N - f.natDegree

theorem Cslib.Circuits.Rational.Expansion.exists_order_echelon_family {K : Type u_1} [Field K] (d : ℕ) (V : Submodule K (Polynomial K)) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ (h : ℕ) (f : Fin h → Polynomial K), LinearIndependent K f ∧ Submodule.span K (Set.range f) = V ∧ Function.Injective fun (i : Fin h) => (f i).natTrailingDegree

theorem Cslib.Circuits.Rational.Expansion.wronskian_linearCombination {K : Type u_1} [CommRing K] {h : ℕ} (f : Fin h → Polynomial K) (A : Matrix (Fin h) (Fin h) K) : (wronskianFamily fun (j : Fin h) => ∑ i : Fin h, A i j • f i) = wronskianFamily f * Polynomial.C A.det

theorem Cslib.Circuits.Rational.Expansion.basis_toMatrix_det_ne_zero {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {h : ℕ} (b b' : Module.Basis (Fin h) K M) : (b.toMatrix ⇑b').det ≠ 0

theorem Cslib.Circuits.Rational.Expansion.wronskian_basis_change {K : Type u_1} [Field K] {h : ℕ} {V : Submodule K (Polynomial K)} (b b' : Module.Basis (Fin h) K ↥V) : (wronskianFamily fun (j : Fin h) => ↑(b' j)) = (wronskianFamily fun (j : Fin h) => ↑(b j)) * Polynomial.C (b.toMatrix ⇑b').det

theorem Cslib.Circuits.Rational.Expansion.exists_order_echelon_basis {K : Type u_1} [Field K] (d : ℕ) (V : Submodule K (Polynomial K)) {h : ℕ} (b : Module.Basis (Fin h) K ↥V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : ∃ (b' : Module.Basis (Fin h) K ↥V), Function.Injective fun (j : Fin h) => (↑(b' j)).natTrailingDegree

theorem Cslib.Circuits.Rational.Expansion.wronskian_basis_ne_zero {K : Type u_1} [Field K] [CharZero K] (d : ℕ) {V : Submodule K (Polynomial K)} {h : ℕ} (b : Module.Basis (Fin h) K ↥V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : (wronskianFamily fun (j : Fin h) => ↑(b j)) ≠ 0

theorem Cslib.Circuits.Rational.Expansion.derivative_taylor {K : Type u_1} [CommRing K] (a : K) (f : Polynomial K) : Polynomial.derivative ((Polynomial.taylor a) f) = (Polynomial.taylor a) (Polynomial.derivative f)

theorem Cslib.Circuits.Rational.Expansion.iterate_derivative_taylor {K : Type u_1} [CommRing K] (a : K) (f : Polynomial K) (r : ℕ) : (⇑Polynomial.derivative)^[r] ((Polynomial.taylor a) f) = (Polynomial.taylor a) ((⇑Polynomial.derivative)^[r] f)

theorem Cslib.Circuits.Rational.Expansion.wronskian_taylor {K : Type u_1} [CommRing K] {h : ℕ} (a : K) (f : Fin h → Polynomial K) : (wronskianFamily fun (j : Fin h) => (Polynomial.taylor a) (f j)) = (Polynomial.taylor a) (wronskianFamily f)

theorem Cslib.Circuits.Rational.Expansion.natDegree_wronskian_le {K : Type u_1} [CommRing K] {h : ℕ} (f : Fin h → Polynomial K) (D : ℕ) (hd : ∀ (j : Fin h), (f j).natDegree ≤ D) : (wronskianFamily f).natDegree ≤ h * D

theorem Cslib.Circuits.Rational.Expansion.sum_rootMultiplicity_le_natDegree {K : Type u_1} [Field K] (f : Polynomial K) (s : Finset K) : ∑ a ∈ s, Polynomial.rootMultiplicity a f ≤ f.natDegree

theorem Cslib.Circuits.Rational.Expansion.wronskian_order_at {K : Type u_1} [Field K] [CharZero K] {h : ℕ} (a : K) (f : Fin h → Polynomial K) (hf : ∀ (j : Fin h), f j ≠ 0) (hd : Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a (f j)) : Polynomial.rootMultiplicity a (wronskianFamily f) + ∑ i : Fin h, ↑i = ∑ j : Fin h, Polynomial.rootMultiplicity a (f j)

theorem Cslib.Circuits.Rational.Expansion.wronskian_basis_rootMultiplicity {K : Type u_1} [Field K] [CharZero K] (d : ℕ) {V : Submodule K (Polynomial K)} {h : ℕ} (b b' : Module.Basis (Fin h) K ↥V) (a : K) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) : Polynomial.rootMultiplicity a (wronskianFamily fun (j : Fin h) => ↑(b' j)) = Polynomial.rootMultiplicity a (wronskianFamily fun (j : Fin h) => ↑(b j))

theorem Cslib.Circuits.Rational.Expansion.wronskian_order_bound {K : Type u_1} [Field K] [CharZero K] (d : ℕ) {V : Submodule K (Polynomial K)} {h w : ℕ} (b : Module.Basis (Fin h) K ↥V) (a : Fin w → K) (ha : Function.Injective a) (e : Fin w → Module.Basis (Fin h) K ↥V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) (he : ∀ (i : Fin w), Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity (a i) ↑((e i) j)) : ∑ i : Fin w, ∑ j : Fin h, Polynomial.rootMultiplicity (a i) ↑((e i) j) ≤ h * (d - 1) + w * ∑ j : Fin h, ↑j

The Wronskian order bound for distinct points of a characteristic-zero field and order-echelon bases. The triangular sum is exactly binom(h,2).

theorem Cslib.Circuits.Rational.Expansion.exists_echelon_basis_at {K : Type u_1} [Field K] (d : ℕ) (V : Submodule K (Polynomial K)) {h : ℕ} (b : Module.Basis (Fin h) K ↥V) (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) (a : K) : ∃ (b' : Module.Basis (Fin h) K ↥V), Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a ↑(b' j)

theorem Cslib.Circuits.Rational.Expansion.low_coefficients_force_zero {K : Type u_1} [Field K] {h : ℕ} (f : Fin h → Polynomial K) (hf : ∀ (j : Fin h), f j ≠ 0) (hd : Function.Injective fun (j : Fin h) => (f j).natTrailingDegree) (c : Fin h → K) (r : ℕ) (hz : ∀ m < r, (∑ j : Fin h, c j • f j).coeff m = 0) (j : Fin h) : (f j).natTrailingDegree < r → c j = 0

Distinct leading orders make vanishing conditions triangular; no linear combination can cancel its first nonzero echelon term.

def Cslib.Circuits.Rational.Expansion.vanishingFiltration {K : Type u_1} [Field K] (V : Submodule K (Polynomial K)) (a : K) (r : ℕ) : Submodule K (Polynomial K)

The exact vanishing filtration, expressed by low Taylor coefficients.

theorem Cslib.Circuits.Rational.Expansion.mem_vanishingFiltration_iff_dvd {K : Type u_1} [Field K] (V : Submodule K (Polynomial K)) (a : K) (r : ℕ) (f : Polynomial K) : f ∈ vanishingFiltration V a r ↔ f ∈ V ∧ (Polynomial.X - Polynomial.C a) ^ r ∣ f

theorem Cslib.Circuits.Rational.Expansion.vanishingFiltration_eq_span {K : Type u_1} [Field K] {V : Submodule K (Polynomial K)} {h : ℕ} (b : Module.Basis (Fin h) K ↥V) (a : K) (hb : Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a ↑(b j)) (r : ℕ) : vanishingFiltration V a r = Submodule.span K (Set.range fun (j : { j : Fin h // r ≤ Polynomial.rootMultiplicity a ↑(b j) }) => ↑(b ↑j))

theorem Cslib.Circuits.Rational.Expansion.finrank_vanishingFiltration {K : Type u_1} [Field K] {V : Submodule K (Polynomial K)} {h : ℕ} (b : Module.Basis (Fin h) K ↥V) (a : K) (hb : Function.Injective fun (j : Fin h) => Polynomial.rootMultiplicity a ↑(b j)) (r : ℕ) : Module.finrank K ↥(vanishingFiltration V a r) = Fintype.card { j : Fin h // r ≤ Polynomial.rootMultiplicity a ↑(b j) }

Row reduction exactly describes the whole vanishing filtration, not only the basis vectors.