Rational hitting lists: wronskian

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Wronskian.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

noncomputable def Complexity.RationalHitting.Expansion.wronskian {K : Type u_1} [CommRing K] {h : ℕ} (f : Fin h → Polynomial K) : Polynomial K

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

Equations

• Complexity.RationalHitting.Expansion.wronskian f = (Matrix.of fun (i j : Fin h) => (⇑Polynomial.derivative)^[↑i] (f j)).det

theorem Complexity.RationalHitting.Expansion.coeff_prod_sum_degrees {K : Type u_1} {ι : Type u_2} [CommSemiring K] (s : Finset ι) (f : ι → Polynomial K) (d : ι → ℕ) (hd : ∀ i ∈ s, (f i).natDegree ≤ d i) : (∏ i ∈ s, f i).coeff (∑ i ∈ s, d i) = ∏ i ∈ s, (f i).coeff (d i)

theorem Complexity.RationalHitting.Expansion.coeff_det_column_degrees {K : Type u_1} {ι : Type u_2} [CommRing K] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι (Polynomial K)) (d : ι → ℕ) (hd : ∀ (i j : ι), (A i j).natDegree ≤ d j) : A.det.coeff (∑ j : ι, d j) = (Matrix.of fun (i j : ι) => (A i j).coeff (d j)).det

theorem Complexity.RationalHitting.Expansion.natDegree_scaled_derivative_le {K : Type u_1} [CommRing K] (f : Polynomial K) (r : ℕ) : (Polynomial.X ^ r * (⇑Polynomial.derivative)^[r] f).natDegree ≤ f.natDegree

theorem Complexity.RationalHitting.Expansion.coeff_scaled_derivative {K : Type u_1} [CommRing K] (f : Polynomial K) (r : ℕ) : (Polynomial.X ^ r * (⇑Polynomial.derivative)^[r] f).coeff f.natDegree = ↑(f.natDegree.descFactorial r) * f.leadingCoeff

theorem Complexity.RationalHitting.Expansion.wronskian_ne_zero_of_distinct_degrees {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).natDegree) : wronskian f ≠ 0

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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) : wronskian f ≠ 0 ∧ (wronskian 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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

• Complexity.RationalHitting.Expansion.reflectLinearEquiv K N = { toFun := Polynomial.reflect N, map_add' := ⋯, map_smul' := ⋯, invFun := Polynomial.reflect N, left_inv := ⋯, right_inv := ⋯ }

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Expansion.wronskian_linearCombination {K : Type u_1} [CommRing K] {h : ℕ} (f : Fin h → Polynomial K) (A : Matrix (Fin h) (Fin h) K) : (wronskian fun (j : Fin h) => ∑ i : Fin h, A i j • f i) = wronskian f * Polynomial.C A.det

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.Expansion.wronskian_basis_change {K : Type u_1} [Field K] {h : ℕ} {V : Submodule K (Polynomial K)} (b b' : Module.Basis (Fin h) K ↥V) : (wronskian fun (j : Fin h) => ↑(b' j)) = (wronskian fun (j : Fin h) => ↑(b j)) * Polynomial.C (b.toMatrix ⇑b').det

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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) : (wronskian fun (j : Fin h) => ↑(b j)) ≠ 0

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Expansion.wronskian_taylor {K : Type u_1} [CommRing K] {h : ℕ} (a : K) (f : Fin h → Polynomial K) : (wronskian fun (j : Fin h) => (Polynomial.taylor a) (f j)) = (Polynomial.taylor a) (wronskian f)

theorem Complexity.RationalHitting.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) : (wronskian f).natDegree ≤ h * D

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 (wronskian f) + ∑ i : Fin h, ↑i = ∑ j : Fin h, Polynomial.rootMultiplicity a (f j)

theorem Complexity.RationalHitting.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 (wronskian fun (j : Fin h) => ↑(b' j)) = Polynomial.rootMultiplicity a (wronskian fun (j : Fin h) => ↑(b j))

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.