Local auxiliary-family Wronskian estimates

This file formalizes completion-level parts of the four local cases in the proof of Corvaja--Zannier's Proposition 2. The functions are Laurent series, and every order hypothesis is stated explicitly. No assertion is made here about embeddings of a global function field into its completions or about summing orders over all places.

The main new ingredients are:

• an indexed ordinary-derivative Wronskian, allowing the source's exact index type Fin k ⊕ (Fin (k + 1) × Fin h);
• the regular-family estimate used in case (ii);
• the explicit lower-unitriangular column matrix used in case (iii), together with its determinant-one proof; and
• the geometric-series identity which improves the first k columns from u ^ j * ρ to u ^ j * v ^ h * ρ.

Source provenance: published pages 1935--1936; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 636--732. Case (ii) is lines 689--691, and the case-(iii) column operation is lines 694--719.

def BGS.CorvajaZannier.indexedLaurentSeriesWronskian {K : Type u_1} [Field K] {ι : Type u_2} (ε : ι → ℕ) (f : ι → LaurentSeries K) : Matrix ι ι (LaurentSeries K)

An ordinary-derivative Wronskian whose rows and columns have an arbitrary common finite index type. The function ε specifies the derivative order of each row.

Equations

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

def BGS.CorvajaZannier.indexedLaurentSeriesColumnCombination {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (f : ι → LaurentSeries K) (A : Matrix ι ι K) : ι → LaurentSeries K

Apply a constant scalar matrix to an indexed Laurent-series family.

Equations

• BGS.CorvajaZannier.indexedLaurentSeriesColumnCombination f A j = ∑ i : ι, A i j • f i

theorem BGS.CorvajaZannier.indexedLaurentSeriesWronskian_columnCombination {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (ε : ι → ℕ) (f : ι → LaurentSeries K) (A : Matrix ι ι K) : indexedLaurentSeriesWronskian ε (indexedLaurentSeriesColumnCombination f A) = indexedLaurentSeriesWronskian ε f * A.map ⇑(algebraMap K (LaurentSeries K))

Constant column operations commute with the indexed ordinary Wronskian.

theorem BGS.CorvajaZannier.indexedLaurentSeriesWronskian_det_columnCombination_of_det_eq_one {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ε : ι → ℕ) (f : ι → LaurentSeries K) (A : Matrix ι ι K) (hA : A.det = 1) : (indexedLaurentSeriesWronskian ε (indexedLaurentSeriesColumnCombination f A)).det = (indexedLaurentSeriesWronskian ε f).det

A determinant-one constant column operation preserves an indexed local Wronskian determinant.

theorem BGS.CorvajaZannier.orderTop_indexedLaurentSeriesWronskian_det_lower_bound {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ε : ι → ℕ) (f : ι → LaurentSeries K) : ↑(∑ j : ι, HahnSeries.order (f j) - ∑ i : ι, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε f).det

The indexed ordinary Wronskian has order at least the sum of its column orders minus the sum of its row derivative orders.

theorem BGS.CorvajaZannier.orderTop_derivative_iterate_nonnegative_of_order_nonnegative {K : Type u_1} [Field K] (r : ℕ) (f : LaurentSeries K) (hf : 0 ≤ HahnSeries.order f) : 0 ≤ HahnSeries.orderTop ((⇑(LaurentSeries.derivative K))^[r] f)

Ordinary differentiation preserves Laurent-series integrality.

theorem BGS.CorvajaZannier.orderTop_indexedLaurentSeriesWronskian_det_nonnegative_of_regular {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ε : ι → ℕ) (f : ι → LaurentSeries K) (hf : ∀ (i : ι), 0 ≤ HahnSeries.order (f i)) : 0 ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε f).det

Case (ii), at the completion level: if every column is regular, then the ordinary-derivative Wronskian determinant is regular.

theorem BGS.CorvajaZannier.orderTop_auxiliaryFamily_caseII_nonnegative {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : LaurentSeries K) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (huOrder : HahnSeries.order u = 0) (hvOrder : HahnSeries.order v = 0) (hratio : 0 ≤ HahnSeries.order ((1 - u) / (1 - v))) : 0 ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (auxiliaryFamily u v h k)).det

Case (ii) connected to the exact auxiliary family. Outside the support of u and v, both have order zero; if the ratio (1-u)/(1-v) is regular, then every auxiliary column is regular and so is its Wronskian determinant.

def BGS.CorvajaZannier.caseIIIGridCorrection {K : Type u_1} [Field K] (h k : ℕ) : Matrix (Fin (k + 1) × Fin h) (Fin k) K

The lower-left block of the case-(iii) column operation. For each first column i, it subtracts every grid column (i,s) and adds every grid column (i+1,s).

Equations

• BGS.CorvajaZannier.caseIIIGridCorrection h k rs i = if rs.1 = i.castSucc then -1 else if rs.1 = i.succ then 1 else 0

def BGS.CorvajaZannier.caseIIIColumnMatrix {K : Type u_1} [Field K] (h k : ℕ) : Matrix (Fin k ⊕ Fin (k + 1) × Fin h) (Fin k ⊕ Fin (k + 1) × Fin h) K

The exact lower-unitriangular constant column matrix used in case (iii).

Equations

• BGS.CorvajaZannier.caseIIIColumnMatrix h k = Matrix.fromBlocks 1 0 (BGS.CorvajaZannier.caseIIIGridCorrection h k) 1

theorem BGS.CorvajaZannier.caseIIIColumnMatrix_det {K : Type u_1} [Field K] (h k : ℕ) : (caseIIIColumnMatrix h k).det = 1

The case-(iii) column matrix has determinant one.

theorem BGS.CorvajaZannier.caseIII_geometricSeries_column_identity {K : Type u_1} [Field K] (u v ρ : LaurentSeries K) (h j : ℕ) (hρ : (1 - v) * ρ = 1 - u) : u ^ j * ρ - u ^ j * (1 - u) * ∑ s ∈ Finset.range h, v ^ s = u ^ j * v ^ h * ρ

The geometric-series identity behind the case-(iii) column operation. The hypothesis is the denominator-cleared identity (1-v)ρ = 1-u.

noncomputable def BGS.CorvajaZannier.localAuxiliaryFamily {K : Type u_1} [Field K] (u v ρ : LaurentSeries K) (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → LaurentSeries K

The source auxiliary family written with ρ as an explicit parameter. This separates the local column algebra from the later specialization ρ = (1-u)/(1-v).

Equations

• BGS.CorvajaZannier.localAuxiliaryFamily u v ρ h k (Sum.inl i) = u ^ ↑i * ρ
• BGS.CorvajaZannier.localAuxiliaryFamily u v ρ h k (Sum.inr rs) = u ^ ↑rs.1 * v ^ ↑rs.2

@[simp]

theorem BGS.CorvajaZannier.localAuxiliaryFamily_div_eq_auxiliaryFamily {K : Type u_1} [Field K] (u v : LaurentSeries K) (h k : ℕ) : localAuxiliaryFamily u v ((1 - u) / (1 - v)) h k = auxiliaryFamily u v h k

Specializing the explicit ratio parameter recovers the auxiliary family from AuxiliaryFamily.

noncomputable def BGS.CorvajaZannier.caseIIIImprovedAuxiliaryFamily {K : Type u_1} [Field K] (u v ρ : LaurentSeries K) (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → LaurentSeries K

The case-(iii) family after replacing its first k columns.

Equations

• BGS.CorvajaZannier.caseIIIImprovedAuxiliaryFamily u v ρ h k (Sum.inl i) = u ^ ↑i * v ^ h * ρ
• BGS.CorvajaZannier.caseIIIImprovedAuxiliaryFamily u v ρ h k (Sum.inr rs) = u ^ ↑rs.1 * v ^ ↑rs.2

theorem BGS.CorvajaZannier.indexedColumnCombination_caseIIIColumnMatrix {K : Type u_1} [Field K] (u v ρ : LaurentSeries K) (h k : ℕ) (hρ : (1 - v) * ρ = 1 - u) : indexedLaurentSeriesColumnCombination (localAuxiliaryFamily u v ρ h k) (caseIIIColumnMatrix h k) = caseIIIImprovedAuxiliaryFamily u v ρ h k

The explicit determinant-one matrix performs exactly the column replacement from case (iii).

theorem BGS.CorvajaZannier.indexedWronskian_det_caseIII_columnReplacement {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v ρ : LaurentSeries K) (hρ : (1 - v) * ρ = 1 - u) : (indexedLaurentSeriesWronskian ε (caseIIIImprovedAuxiliaryFamily u v ρ h k)).det = (indexedLaurentSeriesWronskian ε (localAuxiliaryFamily u v ρ h k)).det

Case (iii), completion-level determinant identity: the Wronskian is unchanged after replacing u^j ρ by u^j v^h ρ in its first k columns.

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_caseIII_lower_bound {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v ρ : LaurentSeries K) (hρ : (1 - v) * ρ = 1 - u) : ↑(∑ j : Fin k ⊕ Fin (k + 1) × Fin h, HahnSeries.order (caseIIIImprovedAuxiliaryFamily u v ρ h k j) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (localAuxiliaryFamily u v ρ h k)).det

Case (iii), completion-level order estimate after the exact source column replacement. The right side retains the column orders explicitly; evaluating those orders from ν(u), ν(v), and ν(ρ) is a separate elementary step.

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_caseIII_source_lower_bound {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v ρ : LaurentSeries K) (hρ : (1 - v) * ρ = 1 - u) (hu : u ≠ 0) (hv : v ≠ 0) (hρ0 : ρ ≠ 0) : ↑((k * (k - 1) / 2) • HahnSeries.order u + (h * k) • HahnSeries.order v + k • HahnSeries.order ρ + ∑ rs : Fin (k + 1) × Fin h, HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (localAuxiliaryFamily u v ρ h k)).det

Case (iii) in the displayed source form. The grid-column contribution is left as the exact sum appearing in the paper; it is the part that cancels by the global product formula after summing over places.

theorem BGS.CorvajaZannier.orderTop_indexedWronskian_det_caseIV_source_lower_bound {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v ρ : LaurentSeries K) (hu : u ≠ 0) (hρ0 : ρ ≠ 0) : ↑((k * (k - 1) / 2) • HahnSeries.order u + k • HahnSeries.order ρ + ∑ rs : Fin (k + 1) × Fin h, HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (localAuxiliaryFamily u v ρ h k)).det

Case (iv), completion-level displayed source estimate: no column operation is made, so the first k columns contribute the triangular u term and the kρ term directly.

theorem BGS.CorvajaZannier.orderTop_auxiliaryFamily_caseIII_source_lower_bound {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : LaurentSeries K) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • HahnSeries.order u + (h * k) • HahnSeries.order v + k • HahnSeries.order ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (auxiliaryFamily u v h k)).det

Case (iii) connected to the exact auxiliary family defined earlier in the formalization. The hypotheses u ≠ 1 and v ≠ 1 ensure that the ratio column is nonzero and that clearing its denominator is sound.

theorem BGS.CorvajaZannier.orderTop_auxiliaryFamily_caseIV_source_lower_bound {K : Type u_1} [Field K] (h k : ℕ) (ε : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : LaurentSeries K) (hu0 : u ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • HahnSeries.order u + k • HahnSeries.order ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, HahnSeries.order (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(ε i)) ≤ HahnSeries.orderTop (indexedLaurentSeriesWronskian ε (auxiliaryFamily u v h k)).det

Case (iv) connected to the exact auxiliary family.