Local Wronskian order estimates

After choosing a local parameter, the Corvaja--Zannier Wronskian becomes a Wronskian of Laurent series. This file proves the determinant-level local estimate: the order of an n × n ordinary Wronskian is at least the sum of the column orders minus n * (n - 1) / 2.

The theorem uses orderTop, so it also covers a vanishing determinant. It is the completion-level inequality in the source argument; embedding a curve's function field in these completions and summing the resulting orders remain separate global geometric obligations.

def BGS.CorvajaZannier.laurentSeriesWronskian {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) : Matrix (Fin n) (Fin n) (LaurentSeries K)

The ordinary Wronskian matrix of Laurent series with respect to the local parameter.

Equations

• BGS.CorvajaZannier.laurentSeriesWronskian f i j = (⇑(LaurentSeries.derivative K))^[↑i] (f j)

def BGS.CorvajaZannier.laurentSeriesColumnCombination {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) (A : Matrix (Fin n) (Fin n) K) : Fin n → LaurentSeries K

Apply a constant scalar matrix to the columns of a Laurent-series family.

Equations

• BGS.CorvajaZannier.laurentSeriesColumnCombination f A j = ∑ i : Fin n, A i j • f i

theorem BGS.CorvajaZannier.laurentSeriesWronskian_columnCombination {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) (A : Matrix (Fin n) (Fin n) K) : laurentSeriesWronskian (laurentSeriesColumnCombination f A) = laurentSeriesWronskian f * A.map ⇑(algebraMap K (LaurentSeries K))

A constant change of columns commutes with formation of the local Wronskian.

theorem BGS.CorvajaZannier.laurentSeriesWronskian_det_columnCombination_of_det_eq_one {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) (A : Matrix (Fin n) (Fin n) K) (hA : A.det = 1) : (laurentSeriesWronskian (laurentSeriesColumnCombination f A)).det = (laurentSeriesWronskian f).det

A determinant-one constant column operation leaves the local Wronskian determinant unchanged. This is the formal column-operation principle used in the source's local cases.

theorem BGS.CorvajaZannier.orderTop_laurentSeriesWronskian_det_lower_bound {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) : ↑(∑ j : Fin n, HahnSeries.order (f j) - ∑ j : Fin n, ↑↑j) ≤ HahnSeries.orderTop (laurentSeriesWronskian f).det

Before evaluating the triangular number, the local Wronskian determinant has order at least the sum of the column orders minus the sum of the derivative orders 0, ..., n - 1.

theorem BGS.CorvajaZannier.orderTop_laurentSeriesWronskian_det_lower_bound_closed {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) : ↑(∑ j : Fin n, HahnSeries.order (f j) - ↑(n * (n - 1) / 2)) ≤ HahnSeries.orderTop (laurentSeriesWronskian f).det

The local Wronskian determinant loses at most the triangular number n * (n - 1) / 2 from the sum of its column orders.

theorem BGS.CorvajaZannier.orderTop_laurentSeriesWronskian_det_lower_bound_after_columnCombination {K : Type u_1} [Field K] {n : ℕ} (f : Fin n → LaurentSeries K) (A : Matrix (Fin n) (Fin n) K) (hA : A.det = 1) : ↑(∑ j : Fin n, HahnSeries.order (laurentSeriesColumnCombination f A j) - ↑(n * (n - 1) / 2)) ≤ HahnSeries.orderTop (laurentSeriesWronskian f).det

The determinant order can be estimated after any determinant-one constant column operation. This is the form used when the source separates repeated pole orders or replaces columns by better local approximations.