Wronskian.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

An integral frame records integral coordinate functionals, making saturation explicit.

def OAI.RationalHitting.Expansion.wronskian line 12
Source documentation
The Wronskian with derivative orders 0, ..., h - 1.
```
def wronskian {K : Type*} [CommRing K] {h : ℕ} (f : Fin h → K[X]) : K[X] :=
…
```
lemma OAI.RationalHitting.Expansion.coeff_prod_sum_degrees line 15
lemma OAI.RationalHitting.Expansion.coeff_det_column_degrees line 28
lemma OAI.RationalHitting.Expansion.natDegree_scaled_derivative_le line 37
lemma OAI.RationalHitting.Expansion.coeff_scaled_derivative line 50
lemma OAI.RationalHitting.Expansion.wronskian_ne_zero_of_distinct_degrees line 60

lemma OAI.RationalHitting.Expansion.det_factor_column_orders line 114

Source documentation

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

lemma det_factor_column_orders {K ι : Type*} [CommRing K]
    [Fintype ι] [DecidableEq ι] (A : Matrix ι ι K[X]) (d : ι → ℕ)
    (hd : ∀ i j, X ^ d j ∣ A i j) :
    ∃ B : Matrix ι ι K[X],
      A.det = X ^ (∑ j, d j) * B.det ∧
      (∀ i j, (B i j).coeff 0 = (A i j).coeff (d j)) := by
…

lemma OAI.RationalHitting.Expansion.coeff_scaled_derivative_at line 133
lemma OAI.RationalHitting.Expansion.scaled_derivative_order line 143

lemma OAI.RationalHitting.Expansion.wronskian_order_of_distinct_orders line 151

Source documentation

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

lemma wronskian_order_of_distinct_orders {K : Type*} [Field K] [CharZero K]
    {h : ℕ} (f : Fin h → K[X]) (hf : ∀ j, f j ≠ 0)
    (hd : Function.Injective (fun j => (f j).natTrailingDegree)) :
    wronskian f ≠ 0 ∧
      (wronskian f).natTrailingDegree + (∑ i : Fin h, i.val) =
        ∑ j, (f j).natTrailingDegree := by
…

Mentions: OAI.RationalHitting.Expansion.wronskian

lemma OAI.RationalHitting.Expansion.exists_degree_echelon_family line 220

Source documentation

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

lemma exists_degree_echelon_family {K : Type*} [Field K]
    (d : ℕ) (V : Submodule K K[X])
    (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d) :
    ∃ (h : ℕ) (f : Fin h → K[X]), LinearIndependent K f ∧
      Submodule.span K (Set.range f) = V ∧
      Function.Injective (fun i => (f i).natDegree) := by
…

def OAI.RationalHitting.Expansion.reflectLinearEquiv line 312
Source documentation
Fixed-length coefficient reversal is linear, unlike degree-dependent polynomial reversal.
```
def reflectLinearEquiv (K : Type*) [Field K] (N : ℕ) : K[X] ≃ₗ[K] K[X] where
…
```
lemma OAI.RationalHitting.Expansion.order_reflect line 322
lemma OAI.RationalHitting.Expansion.exists_order_echelon_family line 334
lemma OAI.RationalHitting.Expansion.wronskian_linearCombination line 376
lemma OAI.RationalHitting.Expansion.basis_toMatrix_det_ne_zero line 397
lemma OAI.RationalHitting.Expansion.wronskian_basis_change line 404
lemma OAI.RationalHitting.Expansion.exists_order_echelon_basis line 415
lemma OAI.RationalHitting.Expansion.wronskian_basis_ne_zero line 433
lemma OAI.RationalHitting.Expansion.derivative_taylor line 445
lemma OAI.RationalHitting.Expansion.iterate_derivative_taylor line 450
lemma OAI.RationalHitting.Expansion.wronskian_taylor line 458
lemma OAI.RationalHitting.Expansion.natDegree_wronskian_le line 470
lemma OAI.RationalHitting.Expansion.sum_rootMultiplicity_le_natDegree line 485
lemma OAI.RationalHitting.Expansion.wronskian_order_at line 498
lemma OAI.RationalHitting.Expansion.wronskian_basis_rootMultiplicity line 512

theorem OAI.RationalHitting.Expansion.wronskian_order_bound line 525

Source documentation

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 wronskian_order_bound {K : Type*} [Field K] [CharZero K]
    (d : ℕ) {V : Submodule K K[X]} {h w : ℕ}
    (b : Basis (Fin h) K V) (a : Fin w → K) (ha : Function.Injective a)
    (e : Fin w → Basis (Fin h) K V)
    (hV : ∀ f ∈ V, f ≠ 0 → f.natDegree < d)
    (he : ∀ i, Function.Injective (fun j => (e i j : K[X]).rootMultiplicity (a i))) :
    ∑ i, ∑ j, (e i j : K[X]).rootMultiplicity (a i) ≤
      h * (d - 1) + w * (∑ j : Fin h, j.val) := by
…

lemma OAI.RationalHitting.Expansion.exists_echelon_basis_at line 557

lemma OAI.RationalHitting.Expansion.low_coefficients_force_zero line 584

Source documentation

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

lemma low_coefficients_force_zero {K : Type*} [Field K] {h : ℕ}
    (f : Fin h → K[X]) (hf : ∀ j, f j ≠ 0)
    (hd : Function.Injective (fun j => (f j).natTrailingDegree))
    (c : Fin h → K) (r : ℕ)
    (hz : ∀ m < r, (∑ j, c j • f j).coeff m = 0) :
    ∀ j, (f j).natTrailingDegree < r → c j = 0 := by
…

def OAI.RationalHitting.Expansion.vanishingFiltration line 619
Source documentation
The exact vanishing filtration, expressed by low Taylor coefficients.
```
def vanishingFiltration {K : Type*} [Field K] (V : Submodule K K[X])
    (a : K) (r : ℕ) : Submodule K K[X] where
…
```
lemma OAI.RationalHitting.Expansion.mem_vanishingFiltration_iff_dvd line 634
lemma OAI.RationalHitting.Expansion.vanishingFiltration_eq_span line 641

theorem OAI.RationalHitting.Expansion.finrank_vanishingFiltration line 697

Source documentation

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

theorem finrank_vanishingFiltration {K : Type*} [Field K]
    {V : Submodule K K[X]} {h : ℕ} (b : Basis (Fin h) K V)
    (a : K) (hb : Function.Injective (fun j => (b j : K[X]).rootMultiplicity a))
    (r : ℕ) :
    finrank K (vanishingFiltration V a r) =
      Fintype.card {j : Fin h // r ≤ (b j : K[X]).rootMultiplicity a} := by
…

Mentions: OAI.RationalHitting.Expansion.vanishingFiltration